<?xml version="1.0"?>
<div><span class="kw">theorem </span><span class="lab"><font color="Green" title="E4">Th4</font></span>: <a NAME="T4"><span class="comment"><font color="firebrick">:: QUANTAL1:4</font></span><br/></a><div class="add"> for <font color="Olive" title="b1">Q</font> being   non  <a href="struct_0.html#V2" title="STRUCT_0:attr.2">empty</a>   <a href="quantal1.html#L1" title="QUANTAL1:struct.1">QuantaleStr</a>   st  <a href="lattices.html#G3" title="LATTICES:aggr.3">LattStr</a>(#  the <a href="struct_0.html#U1" title="STRUCT_0:sel.1">carrier</a> of <font color="Olive" title="b1">Q</font>, the <a href="lattices.html#U2" title="LATTICES:sel.2">L_join</a> of <font color="Olive" title="b1">Q</font>, the <a href="lattices.html#U1" title="LATTICES:sel.1">L_meet</a> of <font color="Olive" title="b1">Q</font> #) <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="lattice3.html#K1" title="LATTICE3:func.1">BooleLatt</a> <a href="xboole_0.html#K1" title="XBOOLE_0:func.1">{}</a> holds <br/>( <font color="Olive" title="b1">Q</font> is  <a href="group_1.html#V3" title="GROUP_1:attr.3">associative</a>  &amp; <font color="Olive" title="b1">Q</font> is  <a href="group_1.html#V5" title="GROUP_1:attr.5">commutative</a>  &amp; <font color="Olive" title="b1">Q</font> is  <a href="group_1.html#V1" title="GROUP_1:attr.1">unital</a>  &amp; <font color="Olive" title="b1">Q</font> is  <a href="quantal1.html#V6" title="QUANTAL1:attr.6">with_zero</a>  &amp; <font color="Olive" title="b1">Q</font> is  <a href="lattice3.html#V4" title="LATTICE3:attr.4">complete</a>  &amp; <font color="Olive" title="b1">Q</font> is  <a href="quantal1.html#V7" title="QUANTAL1:attr.7">right-distributive</a>  &amp; <font color="Olive" title="b1">Q</font> is  <a href="quantal1.html#V8" title="QUANTAL1:attr.8">left-distributive</a>  &amp; <font color="Olive" title="b1">Q</font> is  <a href="lattices.html#V10" title="LATTICES:attr.10">Lattice-like</a>  )</div></div>
