<?xml version="1.0"?>
<div><span class="kw">theorem </span><span class="lab"><font color="Green" title="E69">Th64</font></span>: <a NAME="T78"><span class="comment"><font color="firebrick">:: CARDFIL4:78</font></span><br/></a><div class="add"> <a href="ordinal1.html#K5" title="ORDINAL1:func.5">0</a>  <a href="tarski.html#R2" title="TARSKI:pred.2">in</a>  <a href="cardfil2.html#K18" title="CARDFIL2:func.18">lim_filter</a> (<span class="p1">(<span class="default"><a href="cardfil4.html#K7" title="CARDFIL4:func.7">#</a> <a href="cardfil4.html#K8" title="CARDFIL4:func.8">dblseq_ex_1</a></span>)</span>,<span class="p1"><a href="cardfil4.html#K2" title="CARDFIL4:func.2">&lt;.</a><span class="default"><span class="p2">(<span class="default"><a href="card_fil.html#K4" title="CARD_FIL:func.4">Frechet_Filter</a> <a href="numbers.html#NK1" title="NUMBERS:NK.1">NAT</a></span>)</span>,<span class="p2">(<span class="default"><a href="card_fil.html#K4" title="CARD_FIL:func.4">Frechet_Filter</a> <a href="numbers.html#NK1" title="NUMBERS:NK.1">NAT</a></span>)</span></span><a href="cardfil4.html#K2" title="CARDFIL4:func.2">.)</a></span>) <span class="kw">by</span> <span class="lab"><a class="ref" href="cardfil4.html#T77" target="_self" onmouseover="rs('cardfil4/T77')" onmouseout="rh()">Th63</a>, <a class="ref" href="cardfil4.html#T71" target="_self" onmouseover="rs('cardfil4/T71')" onmouseout="rh()">Th58</a></span>;<br/></div></div>
