<?xml version="1.0"?>
<div class="add">

<span class="kw">thus </span><a NAME="E1:58_1_1"/>
( ( for <font color="Olive" title="b1">p</font>, <font color="Olive" title="b2">q</font> being  <a href="struct_0.html#NM1" title="STRUCT_0:NM.1">Element</a> of <a href="nat_lat.html#K3" title="NAT_LAT:func.3">Nat_Lattice</a>  holds  <font color="Olive" title="b1">p</font> <a href="lattices.html#K1" title="LATTICES:func.1">"\/"</a> <font color="Olive" title="b2">q</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <font color="Olive" title="b2">q</font> <a href="lattices.html#K1" title="LATTICES:func.1">"\/"</a> <font color="Olive" title="b1">p</font> ) &amp; ( for <font color="Olive" title="b1">p</font>, <font color="Olive" title="b2">q</font>, <font color="Olive" title="b3">r</font> being  <a href="struct_0.html#NM1" title="STRUCT_0:NM.1">Element</a> of <a href="nat_lat.html#K3" title="NAT_LAT:func.3">Nat_Lattice</a>  holds  <font color="Olive" title="b1">p</font> <a href="lattices.html#K1" title="LATTICES:func.1">"\/"</a> <span class="p1">(<span class="default"><font color="Olive" title="b2">q</font> <a href="lattices.html#K1" title="LATTICES:func.1">"\/"</a> <font color="Olive" title="b3">r</font></span>)</span> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <span class="p1">(<span class="default"><font color="Olive" title="b1">p</font> <a href="lattices.html#K1" title="LATTICES:func.1">"\/"</a> <font color="Olive" title="b2">q</font></span>)</span> <a href="lattices.html#K1" title="LATTICES:func.1">"\/"</a> <font color="Olive" title="b3">r</font> ) &amp; ( for <font color="Olive" title="b1">p</font>, <font color="Olive" title="b2">q</font> being  <a href="struct_0.html#NM1" title="STRUCT_0:NM.1">Element</a> of <a href="nat_lat.html#K3" title="NAT_LAT:func.3">Nat_Lattice</a>  holds  <span class="p1">(<span class="default"><font color="Olive" title="b1">p</font> <a href="lattices.html#K2" title="LATTICES:func.2">"/\"</a> <font color="Olive" title="b2">q</font></span>)</span> <a href="lattices.html#K1" title="LATTICES:func.1">"\/"</a> <font color="Olive" title="b2">q</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <font color="Olive" title="b2">q</font> ) &amp; ( for <font color="Olive" title="b1">p</font>, <font color="Olive" title="b2">q</font> being  <a href="struct_0.html#NM1" title="STRUCT_0:NM.1">Element</a> of <a href="nat_lat.html#K3" title="NAT_LAT:func.3">Nat_Lattice</a>  holds  <font color="Olive" title="b1">p</font> <a href="lattices.html#K2" title="LATTICES:func.2">"/\"</a> <font color="Olive" title="b2">q</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <font color="Olive" title="b2">q</font> <a href="lattices.html#K2" title="LATTICES:func.2">"/\"</a> <font color="Olive" title="b1">p</font> ) &amp; ( for <font color="Olive" title="b1">p</font>, <font color="Olive" title="b2">q</font>, <font color="Olive" title="b3">r</font> being  <a href="struct_0.html#NM1" title="STRUCT_0:NM.1">Element</a> of <a href="nat_lat.html#K3" title="NAT_LAT:func.3">Nat_Lattice</a>  holds  <font color="Olive" title="b1">p</font> <a href="lattices.html#K2" title="LATTICES:func.2">"/\"</a> <span class="p1">(<span class="default"><font color="Olive" title="b2">q</font> <a href="lattices.html#K2" title="LATTICES:func.2">"/\"</a> <font color="Olive" title="b3">r</font></span>)</span> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <span class="p1">(<span class="default"><font color="Olive" title="b1">p</font> <a href="lattices.html#K2" title="LATTICES:func.2">"/\"</a> <font color="Olive" title="b2">q</font></span>)</span> <a href="lattices.html#K2" title="LATTICES:func.2">"/\"</a> <font color="Olive" title="b3">r</font> ) &amp; ( for <font color="Olive" title="b1">p</font>, <font color="Olive" title="b2">q</font> being  <a href="struct_0.html#NM1" title="STRUCT_0:NM.1">Element</a> of <a href="nat_lat.html#K3" title="NAT_LAT:func.3">Nat_Lattice</a>  holds  <font color="Olive" title="b1">p</font> <a href="lattices.html#K2" title="LATTICES:func.2">"/\"</a> <span class="p1">(<span class="default"><font color="Olive" title="b1">p</font> <a href="lattices.html#K1" title="LATTICES:func.1">"\/"</a> <font color="Olive" title="b2">q</font></span>)</span> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <font color="Olive" title="b1">p</font> ) )
 <span class="kw">by</span> <span class="lab"><a class="ref" href="newton.html#T56" title="NEWTON:th.56">NEWTON:56</a>, <a class="ref" href="newton.html#T61" title="NEWTON:th.61">NEWTON:61</a>, <a class="ref" href="newton.html#T66" title="NEWTON:th.66">NEWTON:66</a>, <a class="ref" href="newton.html#T67" title="NEWTON:th.67">NEWTON:67</a></span>; <span class="comment"><font color="Red">:: according to </font></span><a class="ref" href="lattices.html#D4" title="LATTICES:def.4">LATTICES:def 4</a>,<a class="ref" href="lattices.html#D5" title="LATTICES:def.5">LATTICES:def 5</a>,<a class="ref" href="lattices.html#D6" title="LATTICES:def.6">LATTICES:def 6</a>,<a class="ref" href="lattices.html#D7" title="LATTICES:def.7">LATTICES:def 7</a>,<a class="ref" href="lattices.html#D8" title="LATTICES:def.8">LATTICES:def 8</a>,<a class="ref" href="lattices.html#D9" title="LATTICES:def.9">LATTICES:def 9</a>,<a class="ref" href="lattices.html#D10" title="LATTICES:def.10">LATTICES:def 10</a> <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="Red">::  thesis: </font></span></a><span class="hide"> verum</span><br/>


</div>
