<?xml version="1.0"?>
<div><span class="kw">theorem </span><span class="lab"><font color="Green" title="E20">Th17</font></span>: <a NAME="T17"><span class="comment"><font color="firebrick">:: CLASSES5:17</font></span><br/></a><div class="add">(  <a href="tarski.html#K3" title="TARSKI:func.3">union</a> <span class="p1"><a href="tarski.html#K1" title="TARSKI:func.1">{</a><span class="default"><a href="numbers.html#NK1" title="NUMBERS:NK.1">NAT</a></span><a href="tarski.html#K1" title="TARSKI:func.1">}</a></span> <a href="tarski.html#R1" title="TARSKI:pred.1">c=</a>  <a href="classes2.html#K13" title="CLASSES2:func.13">FinSETS</a>  &amp;  not  <a href="tarski.html#K3" title="TARSKI:func.3">union</a> <span class="p1"><a href="tarski.html#K1" title="TARSKI:func.1">{</a><span class="default"><a href="numbers.html#NK1" title="NUMBERS:NK.1">NAT</a></span><a href="tarski.html#K1" title="TARSKI:func.1">}</a></span> <a href="tarski.html#R2" title="TARSKI:pred.2">in</a>  <a href="classes2.html#K13" title="CLASSES2:func.13">FinSETS</a>  &amp;  not <span class="p1"><a href="tarski.html#K1" title="TARSKI:func.1">{</a><span class="default"><a href="numbers.html#NK1" title="NUMBERS:NK.1">NAT</a></span><a href="tarski.html#K1" title="TARSKI:func.1">}</a></span> <a href="tarski.html#R1" title="TARSKI:pred.1">c=</a>  <a href="classes2.html#K13" title="CLASSES2:func.13">FinSETS</a>  &amp;  not <span class="p1"><a href="tarski.html#K1" title="TARSKI:func.1">{</a><span class="default"><a href="numbers.html#NK1" title="NUMBERS:NK.1">NAT</a></span><a href="tarski.html#K1" title="TARSKI:func.1">}</a></span> <a href="tarski.html#R2" title="TARSKI:pred.2">in</a>  <a href="classes2.html#K13" title="CLASSES2:func.13">FinSETS</a>  )</div></div>
