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

<span class="kw">let </span><font color="Maroon" title="c1">S</font> be   <a href="fomodel1.html#NM2" title="FOMODEL1:NM.2">Language</a>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide">  for <font color="Olive" title="b1">D2</font> being  2 <a href="fomodel4.html#V12" title="FOMODEL4:attr.12">-ranked</a>  <a href="fomodel4.html#NM2" title="FOMODEL4:NM.2">RuleSet</a> of <font color="Maroon" title="c1">S</font><br/>  for <font color="Olive" title="b2">X</font> being   <a href="funct_1.html#V4" title="FUNCT_1:attr.4">functional</a>   <a href="hidden.html#M1" title="HIDDEN:mode.1">set</a>   st  <a href="fomodel2.html#K33" title="FOMODEL2:func.33">AllFormulasOf</a> <font color="Maroon" title="c1">S</font> is  <a href="card_3.html#V4" title="CARD_3:attr.4">countable</a>  &amp;  not <span class="p1">(<span class="default"><a href="fomodel1.html#K16" title="FOMODEL1:func.16">LettersOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="subset_1.html#K7" title="SUBSET_1:func.7">\</a> <span class="p1">(<span class="default"><a href="fomodel0.html#K21" title="FOMODEL0:func.21">SymbolsOf</a> <span class="p2">(<span class="default"><font color="Olive" title="b2">X</font> <a href="subset_1.html#K9" title="SUBSET_1:func.9">/\</a> <span class="p3">(<span class="default"><span class="p4">(<span class="default"><span class="p5">(<span class="default"><a href="fomodel1.html#K1" title="FOMODEL1:func.1">AllSymbolsOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="finseq_2.html#K3" title="FINSEQ_2:func.3">*</a></span>)</span> <a href="subset_1.html#K6" title="SUBSET_1:func.6">\</a> <span class="p4"><a href="tarski.html#K1" title="TARSKI:func.1">{</a><span class="default"><a href="xboole_0.html#K1" title="XBOOLE_0:func.1">{}</a></span><a href="tarski.html#K1" title="TARSKI:func.1">}</a></span></span>)</span></span>)</span></span>)</span> is  <a href="finset_1.html#V1" title="FINSET_1:attr.1">finite</a>  &amp;  not <font color="Olive" title="b2">X</font> is <font color="Olive" title="b1">D2</font> <a href="fomodel4.html#V14" title="FOMODEL4:attr.14">-inconsistent</a>  &amp; <font color="Olive" title="b1">D2</font> is  <a href="fomodel4.html#V6" title="FOMODEL4:attr.6">isotone</a>  holds <br/> ex <font color="Olive" title="b3">U</font> being   non  <a href="xboole_0.html#V1" title="XBOOLE_0:attr.1">empty</a>   <a href="hidden.html#M1" title="HIDDEN:mode.1">set</a>  ex <font color="Olive" title="b4">I</font> being    <a href="subset_1.html#M2" title="SUBSET_1:mode.2">Element</a> of <font color="Olive" title="b3">U</font> <a href="fomodel2.html#K16" title="FOMODEL2:func.16">-InterpretersOf</a> <font color="Maroon" title="c1">S</font> st <font color="Olive" title="b2">X</font> is <font color="Olive" title="b4">I</font> <a href="fomodel2.html#V10" title="FOMODEL2:attr.10">-satisfied</a> </span><br/><span class="kw">let </span><font color="Maroon" title="c2">D2</font> be  2 <a href="fomodel4.html#V12" title="FOMODEL4:attr.12">-ranked</a>  <a href="fomodel4.html#NM2" title="FOMODEL4:NM.2">RuleSet</a> of <font color="Maroon" title="c1">S</font>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide">  for <font color="Olive" title="b1">X</font> being   <a href="funct_1.html#V4" title="FUNCT_1:attr.4">functional</a>   <a href="hidden.html#M1" title="HIDDEN:mode.1">set</a>   st  <a href="fomodel2.html#K33" title="FOMODEL2:func.33">AllFormulasOf</a> <font color="Maroon" title="c1">S</font> is  <a href="card_3.html#V4" title="CARD_3:attr.4">countable</a>  &amp;  not <span class="p1">(<span class="default"><a href="fomodel1.html#K16" title="FOMODEL1:func.16">LettersOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="subset_1.html#K7" title="SUBSET_1:func.7">\</a> <span class="p1">(<span class="default"><a href="fomodel0.html#K21" title="FOMODEL0:func.21">SymbolsOf</a> <span class="p2">(<span class="default"><font color="Olive" title="b1">X</font> <a href="subset_1.html#K9" title="SUBSET_1:func.9">/\</a> <span class="p3">(<span class="default"><span class="p4">(<span class="default"><span class="p5">(<span class="default"><a href="fomodel1.html#K1" title="FOMODEL1:func.1">AllSymbolsOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="finseq_2.html#K3" title="FINSEQ_2:func.3">*</a></span>)</span> <a href="subset_1.html#K6" title="SUBSET_1:func.6">\</a> <span class="p4"><a href="tarski.html#K1" title="TARSKI:func.1">{</a><span class="default"><a href="xboole_0.html#K1" title="XBOOLE_0:func.1">{}</a></span><a href="tarski.html#K1" title="TARSKI:func.1">}</a></span></span>)</span></span>)</span></span>)</span> is  <a href="finset_1.html#V1" title="FINSET_1:attr.1">finite</a>  &amp;  not <font color="Olive" title="b1">X</font> is <font color="Maroon" title="c2">D2</font> <a href="fomodel4.html#V14" title="FOMODEL4:attr.14">-inconsistent</a>  &amp; <font color="Maroon" title="c2">D2</font> is  <a href="fomodel4.html#V6" title="FOMODEL4:attr.6">isotone</a>  holds <br/> ex <font color="Olive" title="b2">U</font> being   non  <a href="xboole_0.html#V1" title="XBOOLE_0:attr.1">empty</a>   <a href="hidden.html#M1" title="HIDDEN:mode.1">set</a>  ex <font color="Olive" title="b3">I</font> being    <a href="subset_1.html#M2" title="SUBSET_1:mode.2">Element</a> of <font color="Olive" title="b2">U</font> <a href="fomodel2.html#K16" title="FOMODEL2:func.16">-InterpretersOf</a> <font color="Maroon" title="c1">S</font> st <font color="Olive" title="b1">X</font> is <font color="Olive" title="b3">I</font> <a href="fomodel2.html#V10" title="FOMODEL2:attr.10">-satisfied</a> </span><br/><span class="kw">let </span><font color="Maroon" title="c3">X</font> be   <a href="funct_1.html#V4" title="FUNCT_1:attr.4">functional</a>   <a href="hidden.html#M1" title="HIDDEN:mode.1">set</a> ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> (  <a href="fomodel2.html#K33" title="FOMODEL2:func.33">AllFormulasOf</a> <font color="Maroon" title="c1">S</font> is  <a href="card_3.html#V4" title="CARD_3:attr.4">countable</a>  &amp;  not <span class="p1">(<span class="default"><a href="fomodel1.html#K16" title="FOMODEL1:func.16">LettersOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="subset_1.html#K7" title="SUBSET_1:func.7">\</a> <span class="p1">(<span class="default"><a href="fomodel0.html#K21" title="FOMODEL0:func.21">SymbolsOf</a> <span class="p2">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="subset_1.html#K9" title="SUBSET_1:func.9">/\</a> <span class="p3">(<span class="default"><span class="p4">(<span class="default"><span class="p5">(<span class="default"><a href="fomodel1.html#K1" title="FOMODEL1:func.1">AllSymbolsOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="finseq_2.html#K3" title="FINSEQ_2:func.3">*</a></span>)</span> <a href="subset_1.html#K6" title="SUBSET_1:func.6">\</a> <span class="p4"><a href="tarski.html#K1" title="TARSKI:func.1">{</a><span class="default"><a href="xboole_0.html#K1" title="XBOOLE_0:func.1">{}</a></span><a href="tarski.html#K1" title="TARSKI:func.1">}</a></span></span>)</span></span>)</span></span>)</span> is  <a href="finset_1.html#V1" title="FINSET_1:attr.1">finite</a>  &amp;  not <font color="Maroon" title="c3">X</font> is <font color="Maroon" title="c2">D2</font> <a href="fomodel4.html#V14" title="FOMODEL4:attr.14">-inconsistent</a>  &amp; <font color="Maroon" title="c2">D2</font> is  <a href="fomodel4.html#V6" title="FOMODEL4:attr.6">isotone</a>  implies  ex <font color="Olive" title="b1">U</font> being   non  <a href="xboole_0.html#V1" title="XBOOLE_0:attr.1">empty</a>   <a href="hidden.html#M1" title="HIDDEN:mode.1">set</a>  ex <font color="Olive" title="b2">I</font> being    <a href="subset_1.html#M2" title="SUBSET_1:mode.2">Element</a> of <font color="Olive" title="b1">U</font> <a href="fomodel2.html#K16" title="FOMODEL2:func.16">-InterpretersOf</a> <font color="Maroon" title="c1">S</font> st <font color="Maroon" title="c3">X</font> is <font color="Olive" title="b2">I</font> <a href="fomodel2.html#V10" title="FOMODEL2:attr.10">-satisfied</a>  )</span><br/>





<span class="kw">set </span><font color="Maroon" title="c4">EF</font> =  <a href="fomodel2.html#K43" title="FOMODEL2:func.43">ExFormulasOf</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c5">FF</font> =  <a href="fomodel2.html#K33" title="FOMODEL2:func.33">AllFormulasOf</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c6">G0</font> =  <a href="fomodel4.html#K22" title="FOMODEL4:func.22">R0</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c7">G2</font> =  <a href="fomodel4.html#K24" title="FOMODEL4:func.24">R2</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c8">G3a</font> =  <a href="fomodel4.html#K25" title="FOMODEL4:func.25">R3a</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c9">G3b</font> =  <a href="fomodel4.html#K26" title="FOMODEL4:func.26">R3b</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c10">G3d</font> =  <a href="fomodel4.html#K27" title="FOMODEL4:func.27">R3d</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c11">G3e</font> =  <a href="fomodel4.html#K28" title="FOMODEL4:func.28">R3e</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c12">G1</font> =  <a href="fomodel4.html#K23" title="FOMODEL4:func.23">R1</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c13">G4</font> =  <a href="fomodel4.html#K29" title="FOMODEL4:func.29">R4</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c14">G5</font> =  <a href="fomodel4.html#K30" title="FOMODEL4:func.30">R5</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c15">G6</font> =  <a href="fomodel4.html#K31" title="FOMODEL4:func.31">R6</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c16">G7</font> =  <a href="fomodel4.html#K32" title="FOMODEL4:func.32">R7</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c17">G8</font> =  <a href="fomodel4.html#K33" title="FOMODEL4:func.33">R8</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c18">L</font> =  <a href="fomodel1.html#K16" title="FOMODEL1:func.16">LettersOf</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c19">SS</font> =  <a href="fomodel1.html#K1" title="FOMODEL1:func.1">AllSymbolsOf</a> <font color="Maroon" title="c1">S</font>;<br/>
<span class="kw">set </span><font color="Maroon" title="c20">strings</font> = <span class="p1">(<span class="default"><span class="p2">(<span class="default"><a href="fomodel1.html#K1" title="FOMODEL1:func.1">AllSymbolsOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="finseq_2.html#K3" title="FINSEQ_2:func.3">*</a></span>)</span> <a href="subset_1.html#K6" title="SUBSET_1:func.6">\</a> <span class="p1"><a href="tarski.html#K1" title="TARSKI:func.1">{</a><span class="default"><a href="xboole_0.html#K1" title="XBOOLE_0:func.1">{}</a></span><a href="tarski.html#K1" title="TARSKI:func.1">}</a></span>;<br/>
<span class="kw">set </span><font color="Maroon" title="c21">no</font> =  <a href="fomodel0.html#K21" title="FOMODEL0:func.21">SymbolsOf</a> <span class="p1">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="subset_1.html#K9" title="SUBSET_1:func.9">/\</a> <span class="p2">(<span class="default"><span class="p3">(<span class="default"><span class="p4">(<span class="default"><a href="fomodel1.html#K1" title="FOMODEL1:func.1">AllSymbolsOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="finseq_2.html#K3" title="FINSEQ_2:func.3">*</a></span>)</span> <a href="subset_1.html#K6" title="SUBSET_1:func.6">\</a> <span class="p3"><a href="tarski.html#K1" title="TARSKI:func.1">{</a><span class="default"><a href="xboole_0.html#K1" title="XBOOLE_0:func.1">{}</a></span><a href="tarski.html#K1" title="TARSKI:func.1">}</a></span></span>)</span></span>)</span>;<br/>
<span class="kw">set </span><font color="Maroon" title="c22">D</font> = <font color="Maroon" title="c2">D2</font>;<br/>
<span class="kw">reconsider </span><font color="Maroon" title="c23">D1</font> = <font color="Maroon" title="c2">D2</font> as   <a href="numbers.html#K6" title="NUMBERS:func.6">0</a>  <a href="fomodel4.html#V12" title="FOMODEL4:attr.12">-ranked</a>  1 <a href="fomodel4.html#V12" title="FOMODEL4:attr.12">-ranked</a>  <a href="fomodel4.html#NM2" title="FOMODEL4:NM.2">RuleSet</a> of <font color="Maroon" title="c1">S</font> ;<br/>
<span class="kw">assume </span><a NAME="E2:252"/>
 <a href="fomodel2.html#K33" title="FOMODEL2:func.33">AllFormulasOf</a> <font color="Maroon" title="c1">S</font> is  <a href="card_3.html#V4" title="CARD_3:attr.4">countable</a> 
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> ( <span class="p1">(<span class="default"><a href="fomodel1.html#K16" title="FOMODEL1:func.16">LettersOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="subset_1.html#K7" title="SUBSET_1:func.7">\</a> <span class="p1">(<span class="default"><a href="fomodel0.html#K21" title="FOMODEL0:func.21">SymbolsOf</a> <span class="p2">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="subset_1.html#K9" title="SUBSET_1:func.9">/\</a> <span class="p3">(<span class="default"><span class="p4">(<span class="default"><span class="p5">(<span class="default"><a href="fomodel1.html#K1" title="FOMODEL1:func.1">AllSymbolsOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="finseq_2.html#K3" title="FINSEQ_2:func.3">*</a></span>)</span> <a href="subset_1.html#K6" title="SUBSET_1:func.6">\</a> <span class="p4"><a href="tarski.html#K1" title="TARSKI:func.1">{</a><span class="default"><a href="xboole_0.html#K1" title="XBOOLE_0:func.1">{}</a></span><a href="tarski.html#K1" title="TARSKI:func.1">}</a></span></span>)</span></span>)</span></span>)</span> is  <a href="finset_1.html#V1" title="FINSET_1:attr.1">finite</a>  or <font color="Maroon" title="c3">X</font> is <font color="Maroon" title="c2">D2</font> <a href="fomodel4.html#V14" title="FOMODEL4:attr.14">-inconsistent</a>  or  not <font color="Maroon" title="c2">D2</font> is  <a href="fomodel4.html#V6" title="FOMODEL4:attr.6">isotone</a>  or  ex <font color="Olive" title="b1">U</font> being   non  <a href="xboole_0.html#V1" title="XBOOLE_0:attr.1">empty</a>   <a href="hidden.html#M1" title="HIDDEN:mode.1">set</a>  ex <font color="Olive" title="b2">I</font> being    <a href="subset_1.html#M2" title="SUBSET_1:mode.2">Element</a> of <font color="Olive" title="b1">U</font> <a href="fomodel2.html#K16" title="FOMODEL2:func.16">-InterpretersOf</a> <font color="Maroon" title="c1">S</font> st <font color="Maroon" title="c3">X</font> is <font color="Olive" title="b2">I</font> <a href="fomodel2.html#V10" title="FOMODEL2:attr.10">-satisfied</a>  )</span><br/>

<span class="kw">then </span><span class="kw">reconsider </span><font color="Maroon" title="c24">FFC</font> =  <a href="fomodel2.html#K33" title="FOMODEL2:func.33">AllFormulasOf</a> <font color="Maroon" title="c1">S</font> as   <a href="card_3.html#V4" title="CARD_3:attr.4">countable</a>   <a href="hidden.html#M1" title="HIDDEN:mode.1">set</a>  ;<br/>
<span class="kw">consider </span><font color="Maroon" title="c25">numaa</font> being   <a href="funct_2.html#NM1" title="FUNCT_2:NM.1">Function</a> of <a href="numbers.html#K5" title="NUMBERS:func.5">NAT</a>,<span class="p1">(<span class="default"><span class="p2">(<span class="default"><span class="p3">(<span class="default"><a href="fomodel1.html#K1" title="FOMODEL1:func.1">AllSymbolsOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="finseq_2.html#K3" title="FINSEQ_2:func.3">*</a></span>)</span> <a href="subset_1.html#K6" title="SUBSET_1:func.6">\</a> <span class="p2"><a href="tarski.html#K1" title="TARSKI:func.1">{</a><span class="default"><a href="xboole_0.html#K1" title="XBOOLE_0:func.1">{}</a></span><a href="tarski.html#K1" title="TARSKI:func.1">}</a></span></span>)</span><span class="kw"> such that </span><br/><a NAME="E5:252"/><span class="lab"><font color="Green" title="E137">B10</font></span>: 
<font color="Maroon" title="c24">FFC</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="relat_1.html#K2" title="RELAT_1:func.2">rng</a> <font color="Maroon" title="c25">numaa</font>
 <span class="kw">by</span> <span class="lab"><a class="ref" href="supinf_2.html#D8" title="SUPINF_2:def.8">SUPINF_2:def 8</a></span>;<br/>
<span class="kw">reconsider </span><font color="Maroon" title="c26">numa</font> = <font color="Maroon" title="c25">numaa</font> as   <a href="funct_2.html#NM1" title="FUNCT_2:NM.1">Function</a> of <a href="numbers.html#K5" title="NUMBERS:func.5">NAT</a>,<span class="p1">(<span class="default"><a href="fomodel2.html#K33" title="FOMODEL2:func.33">AllFormulasOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <span class="kw">by</span> <span class="lab"><a class="txt" href="#E5:252"><span class="lab"><font color="Green" title="E137">B10</font></span></a>, <a class="ref" href="funct_2.html#T6" title="FUNCT_2:th.6">FUNCT_2:6</a></span>;<br/>
<a NAME="E7:252"/>
<span class="p1">(<span class="default"><a href="fomodel2.html#K43" title="FOMODEL2:func.43">ExFormulasOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="subset_1.html#K7" title="SUBSET_1:func.7">\</a> <font color="Maroon" title="c24">FFC</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="xboole_0.html#K1" title="XBOOLE_0:func.1">{}</a> 
 
;<br/>
<span class="kw">then </span><span class="kw">reconsider </span><font color="Maroon" title="c27">EFC</font> =  <a href="fomodel2.html#K43" title="FOMODEL2:func.43">ExFormulasOf</a> <font color="Maroon" title="c1">S</font> as   <a href="subset_1.html#NM2" title="SUBSET_1:NM.2">Subset</a> of <font color="Maroon" title="c24">FFC</font> <span class="kw">by</span> <span class="lab"><a class="ref" href="xboole_1.html#T37" title="XBOOLE_1:th.37">XBOOLE_1:37</a></span>;<br/>
<span class="kw">consider </span><font color="Maroon" title="c28">numee</font> being   <a href="funct_2.html#NM1" title="FUNCT_2:NM.1">Function</a> of <a href="numbers.html#K5" title="NUMBERS:func.5">NAT</a>,<font color="Maroon" title="c24">FFC</font><span class="kw"> such that </span><br/><a NAME="E10:252"/><span class="lab"><font color="Green" title="E138">B6</font></span>: 
<font color="Maroon" title="c27">EFC</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="relat_1.html#K2" title="RELAT_1:func.2">rng</a> <font color="Maroon" title="c28">numee</font>
 <span class="kw">by</span> <span class="lab"><a class="ref" href="supinf_2.html#D8" title="SUPINF_2:def.8">SUPINF_2:def 8</a></span>;<br/>
<span class="kw">reconsider </span><font color="Maroon" title="c29">nume</font> = <font color="Maroon" title="c28">numee</font> as   <a href="funct_2.html#NM1" title="FUNCT_2:NM.1">Function</a> of <a href="numbers.html#K5" title="NUMBERS:func.5">NAT</a>,<span class="p1">(<span class="default"><a href="fomodel2.html#K43" title="FOMODEL2:func.43">ExFormulasOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <span class="kw">by</span> <span class="lab"><a class="txt" href="#E10:252"><span class="lab"><font color="Green" title="E138">B6</font></span></a>, <a class="ref" href="funct_2.html#T6" title="FUNCT_2:th.6">FUNCT_2:6</a></span>;<br/>
<span class="kw">assume </span><a NAME="E12:252"/><span class="lab"><font color="Green" title="E139">B0</font></span>: 
(  not <span class="p1">(<span class="default"><a href="fomodel1.html#K16" title="FOMODEL1:func.16">LettersOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="subset_1.html#K7" title="SUBSET_1:func.7">\</a> <span class="p1">(<span class="default"><a href="fomodel0.html#K21" title="FOMODEL0:func.21">SymbolsOf</a> <span class="p2">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="subset_1.html#K9" title="SUBSET_1:func.9">/\</a> <span class="p3">(<span class="default"><span class="p4">(<span class="default"><span class="p5">(<span class="default"><a href="fomodel1.html#K1" title="FOMODEL1:func.1">AllSymbolsOf</a> <font color="Maroon" title="c1">S</font></span>)</span> <a href="finseq_2.html#K3" title="FINSEQ_2:func.3">*</a></span>)</span> <a href="subset_1.html#K6" title="SUBSET_1:func.6">\</a> <span class="p4"><a href="tarski.html#K1" title="TARSKI:func.1">{</a><span class="default"><a href="xboole_0.html#K1" title="XBOOLE_0:func.1">{}</a></span><a href="tarski.html#K1" title="TARSKI:func.1">}</a></span></span>)</span></span>)</span></span>)</span> is  <a href="finset_1.html#V1" title="FINSET_1:attr.1">finite</a>  &amp;  not <font color="Maroon" title="c3">X</font> is <font color="Maroon" title="c2">D2</font> <a href="fomodel4.html#V14" title="FOMODEL4:attr.14">-inconsistent</a>  )
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> (  not <font color="Maroon" title="c2">D2</font> is  <a href="fomodel4.html#V6" title="FOMODEL4:attr.6">isotone</a>  or  ex <font color="Olive" title="b1">U</font> being   non  <a href="xboole_0.html#V1" title="XBOOLE_0:attr.1">empty</a>   <a href="hidden.html#M1" title="HIDDEN:mode.1">set</a>  ex <font color="Olive" title="b2">I</font> being    <a href="subset_1.html#M2" title="SUBSET_1:mode.2">Element</a> of <font color="Olive" title="b1">U</font> <a href="fomodel2.html#K16" title="FOMODEL2:func.16">-InterpretersOf</a> <font color="Maroon" title="c1">S</font> st <font color="Maroon" title="c3">X</font> is <font color="Olive" title="b2">I</font> <a href="fomodel2.html#V10" title="FOMODEL2:attr.10">-satisfied</a>  )</span><br/>

<a NAME="E13:252"/><span class="lab"><font color="Green" title="E140">B1</font></span>: 
(  <a href="fomodel4.html#K22" title="FOMODEL4:func.22">R0</a> <font color="Maroon" title="c1">S</font> <a href="hidden.html#R2" title="HIDDEN:pred.2">in</a> <font color="Maroon" title="c23">D1</font> &amp;  <a href="fomodel4.html#K23" title="FOMODEL4:func.23">R1</a> <font color="Maroon" title="c1">S</font> <a href="hidden.html#R2" title="HIDDEN:pred.2">in</a> <font color="Maroon" title="c2">D2</font> &amp;  <a href="fomodel4.html#K24" title="FOMODEL4:func.24">R2</a> <font color="Maroon" title="c1">S</font> <a href="hidden.html#R2" title="HIDDEN:pred.2">in</a> <font color="Maroon" title="c23">D1</font> &amp;  <a href="fomodel4.html#K29" title="FOMODEL4:func.29">R4</a> <font color="Maroon" title="c1">S</font> <a href="hidden.html#R2" title="HIDDEN:pred.2">in</a> <font color="Maroon" title="c2">D2</font> &amp;  <a href="fomodel4.html#K30" title="FOMODEL4:func.30">R5</a> <font color="Maroon" title="c1">S</font> <a href="hidden.html#R2" title="HIDDEN:pred.2">in</a> <font color="Maroon" title="c2">D2</font> &amp;  <a href="fomodel4.html#K31" title="FOMODEL4:func.31">R6</a> <font color="Maroon" title="c1">S</font> <a href="hidden.html#R2" title="HIDDEN:pred.2">in</a> <font color="Maroon" title="c2">D2</font> &amp;  <a href="fomodel4.html#K32" title="FOMODEL4:func.32">R7</a> <font color="Maroon" title="c1">S</font> <a href="hidden.html#R2" title="HIDDEN:pred.2">in</a> <font color="Maroon" title="c2">D2</font> &amp;  <a href="fomodel4.html#K33" title="FOMODEL4:func.33">R8</a> <font color="Maroon" title="c1">S</font> <a href="hidden.html#R2" title="HIDDEN:pred.2">in</a> <font color="Maroon" title="c2">D2</font> )
 
<span class="kw">by</span> <span class="lab"><a class="ref" href="fomodel4.html#D59" target="_self" title="FOMODEL4:def.59">DefRank</a></span>;<br/>
<span class="kw">set </span><font color="Maroon" title="c30">X1</font> = <font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>);<br/>
<span class="kw">set </span><font color="Maroon" title="c31">X2</font> = (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c26">numa</font>) <a href="fomodel4.html#K49" title="FOMODEL4:func.49">CompletionOf</a> <span class="p1">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>)</span>)</span>;<br/>
<a NAME="E14:252"/><span class="lab"><font color="Green" title="E141">B3</font></span>: 
(<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c26">numa</font>) <a href="fomodel4.html#K49" title="FOMODEL4:func.49">CompletionOf</a> <span class="p1">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>)</span>)</span> is <font color="Maroon" title="c1">S</font> <a href="fomodel2.html#V9" title="FOMODEL2:attr.9">-covering</a> 
 
<span class="kw">by</span> <span class="lab"><a class="txt" href="fomodel4.html#E166"><span class="lab"><font color="Green" title="E134">Lm5</font></span></a>, <a class="txt" href="#E5:252"><span class="lab"><font color="Green" title="E137">B10</font></span></a></span>;<br/>
<span class="kw">assume </span><a NAME="E15:252"/><span class="lab"><font color="Green" title="E142">B2</font></span>: 
<font color="Maroon" title="c2">D2</font> is  <a href="fomodel4.html#V6" title="FOMODEL4:attr.6">isotone</a> 
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide">  ex <font color="Olive" title="b1">U</font> being   non  <a href="xboole_0.html#V1" title="XBOOLE_0:attr.1">empty</a>   <a href="hidden.html#M1" title="HIDDEN:mode.1">set</a>  ex <font color="Olive" title="b2">I</font> being    <a href="subset_1.html#M2" title="SUBSET_1:mode.2">Element</a> of <font color="Olive" title="b1">U</font> <a href="fomodel2.html#K16" title="FOMODEL2:func.16">-InterpretersOf</a> <font color="Maroon" title="c1">S</font> st <font color="Maroon" title="c3">X</font> is <font color="Olive" title="b2">I</font> <a href="fomodel2.html#V10" title="FOMODEL2:attr.10">-satisfied</a> </span><br/>

<a NAME="E16:252"/><span class="kw">then </span>
 not <font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>) is <font color="Maroon" title="c2">D2</font> <a href="fomodel4.html#V14" title="FOMODEL4:attr.14">-inconsistent</a> 
 
<span class="kw">by</span> <span class="lab"><a class="txt" href="fomodel4.html#E160"><span class="lab"><font color="Green" title="E129">Lm6</font></span></a>, <a class="txt" href="#E12:252"><span class="lab"><font color="Green" title="E139">B0</font></span></a>, <a class="txt" href="#E13:252"><span class="lab"><font color="Green" title="E140">B1</font></span></a></span>;<br/>
<a NAME="E17:252"/><span class="kw">then </span><span class="lab"><font color="Green" title="E143">B4</font></span>: 
 not (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c26">numa</font>) <a href="fomodel4.html#K49" title="FOMODEL4:func.49">CompletionOf</a> <span class="p1">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>)</span>)</span> is <font color="Maroon" title="c2">D2</font> <a href="fomodel4.html#V14" title="FOMODEL4:attr.14">-inconsistent</a> 
 
<span class="kw">by</span> <span class="lab"><a class="txt" href="fomodel4.html#E167"><span class="lab"><font color="Green" title="E135">Lm7</font></span></a>, <a class="txt" href="#E15:252"><span class="lab"><font color="Green" title="E142">B2</font></span></a>, <a class="txt" href="#E13:252"><span class="lab"><font color="Green" title="E140">B1</font></span></a></span>;<br/>
<a NAME="E18:252"/><span class="kw">then </span><span class="lab"><font color="Green" title="E144">B5</font></span>: 
( (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c26">numa</font>) <a href="fomodel4.html#K49" title="FOMODEL4:func.49">CompletionOf</a> <span class="p1">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>)</span>)</span> is <font color="Maroon" title="c1">S</font> <a href="fomodel2.html#V6" title="FOMODEL2:attr.6">-mincover</a>  &amp; (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c26">numa</font>) <a href="fomodel4.html#K49" title="FOMODEL4:func.49">CompletionOf</a> <span class="p1">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>)</span>)</span> is <font color="Maroon" title="c2">D2</font> <a href="fomodel4.html#V10" title="FOMODEL4:attr.10">-expanded</a>  )
 
<span class="kw">by</span> <span class="lab"><a class="txt" href="#E13:252"><span class="lab"><font color="Green" title="E140">B1</font></span></a>, <a class="txt" href="fomodel4.html#E137"><span class="lab"><font color="Green" title="E107">Lm8</font></span></a>, <a class="txt" href="#E14:252"><span class="lab"><font color="Green" title="E141">B3</font></span></a></span>;<br/>
<span class="kw">reconsider </span><font color="Maroon" title="c32">X22</font> = (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c26">numa</font>) <a href="fomodel4.html#K49" title="FOMODEL4:func.49">CompletionOf</a> <span class="p1">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>)</span>)</span> as  <font color="Maroon" title="c23">D1</font> <a href="fomodel4.html#V10" title="FOMODEL4:attr.10">-expanded</a>   <a href="hidden.html#M1" title="HIDDEN:mode.1">set</a>  <span class="kw">by</span> <span class="lab"><a class="txt" href="#E13:252"><span class="lab"><font color="Green" title="E140">B1</font></span></a>, <a class="txt" href="fomodel4.html#E137"><span class="lab"><font color="Green" title="E107">Lm8</font></span></a>, <a class="txt" href="#E14:252"><span class="lab"><font color="Green" title="E141">B3</font></span></a>, <a class="txt" href="#E17:252"><span class="lab"><font color="Green" title="E143">B4</font></span></a></span>;<br/>
<span class="kw">take </span><font color="Maroon" title="c33">U</font> =  <a href="eqrel_1.html#K8" title="EQREL_1:func.8">Class</a> <span class="p1">(<span class="default">(<font color="Maroon" title="c32">X22</font>,<font color="Maroon" title="c23">D1</font>) <a href="fomodel4.html#K6" title="FOMODEL4:func.6">-termEq</a></span>)</span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide">  ex <font color="Olive" title="b1">I</font> being    <a href="subset_1.html#M2" title="SUBSET_1:mode.2">Element</a> of <font color="Maroon" title="c33">U</font> <a href="fomodel2.html#K16" title="FOMODEL2:func.16">-InterpretersOf</a> <font color="Maroon" title="c1">S</font> st <font color="Maroon" title="c3">X</font> is <font color="Olive" title="b1">I</font> <a href="fomodel2.html#V10" title="FOMODEL2:attr.10">-satisfied</a> </span><br/>

<span class="kw">reconsider </span><font color="Maroon" title="c34">I</font> = <font color="Maroon" title="c23">D1</font> <a href="fomodel4.html#K39" title="FOMODEL4:func.39">Henkin</a> <font color="Maroon" title="c32">X22</font> as    <a href="subset_1.html#M2" title="SUBSET_1:mode.2">Element</a> of <font color="Maroon" title="c33">U</font> <a href="fomodel2.html#K16" title="FOMODEL2:func.16">-InterpretersOf</a> <font color="Maroon" title="c1">S</font> ;<br/>
<span class="kw">take </span>
<font color="Maroon" title="c34">I</font>
; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> <font color="Maroon" title="c3">X</font> is <font color="Maroon" title="c34">I</font> <a href="fomodel2.html#V10" title="FOMODEL2:attr.10">-satisfied</a> </span><br/>

<a NAME="E21:252"/>
( <font color="Maroon" title="c3">X</font> <a href="subset_1.html#K6" title="SUBSET_1:func.6">\</a> <span class="p1">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>)</span>)</span> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="xboole_0.html#K1" title="XBOOLE_0:func.1">{}</a>  &amp; <span class="p1">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>)</span>)</span> <a href="subset_1.html#K7" title="SUBSET_1:func.7">\</a> <span class="p1">(<span class="default">(<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c26">numa</font>) <a href="fomodel4.html#K49" title="FOMODEL4:func.49">CompletionOf</a> <span class="p2">(<span class="default"><font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>)</span>)</span></span>)</span> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="xboole_0.html#K1" title="XBOOLE_0:func.1">{}</a>  )
 
;<br/>
<a NAME="E22:252"/><span class="kw">then </span><span class="lab"><font color="Green" title="E145">B7</font></span>: 
( <font color="Maroon" title="c3">X</font> <a href="tarski.html#R1" title="TARSKI:pred.1">c=</a> <font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>) &amp; <font color="Maroon" title="c3">X</font> <a href="fomodel4.html#NK47" title="FOMODEL4:NK.47">addw</a> (<font color="Maroon" title="c23">D1</font>,<font color="Maroon" title="c29">nume</font>) <a href="tarski.html#R1" title="TARSKI:pred.1">c=</a> <font color="Maroon" title="c32">X22</font> )
 
<span class="kw">by</span> <span class="lab"><a class="ref" href="xboole_1.html#T37" title="XBOOLE_1:th.37">XBOOLE_1:37</a></span>;<br/>
<a NAME="E23:252"/><span class="kw">then </span><span class="lab"><font color="Green" title="E146">BB9</font></span>: 
<font color="Maroon" title="c32">X22</font> is <font color="Maroon" title="c1">S</font> <a href="fomodel4.html#V15" title="FOMODEL4:attr.15">-witnessed</a> 
 
<span class="kw">by</span> <span class="lab"><a class="ref" href="fomodel4.html#T18" target="_self" title="FOMODEL4:th.18">Th19</a>, <a class="txt" href="#E12:252"><span class="lab"><font color="Green" title="E139">B0</font></span></a>, <a class="txt" href="#E13:252"><span class="lab"><font color="Green" title="E140">B1</font></span></a>, <a class="txt" href="#E15:252"><span class="lab"><font color="Green" title="E142">B2</font></span></a>, <a class="txt" href="#E17:252"><span class="lab"><font color="Green" title="E143">B4</font></span></a>, <a class="txt" href="#E10:252"><span class="lab"><font color="Green" title="E138">B6</font></span></a></span>;<br/>
<div><span class="kw">hereby </span> <span class="comment"><font color="firebrick">:: according to </font></span><a class="ref" href="fomodel2.html#D42" title="FOMODEL2:def.42">FOMODEL2:def 42</a> <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span>
<div class="add"><span class="kw">let </span><font color="Maroon" title="c35">phi</font> be   <a href="fomodel2.html#V4" title="FOMODEL2:attr.4">wff</a>  <a href="fomodel1.html#NM3" title="FOMODEL1:NM.3">string</a> of <font color="Maroon" title="c1">S</font>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> ( <font color="Maroon" title="c35">phi</font> <a href="hidden.html#R2" title="HIDDEN:pred.2">in</a> <font color="Maroon" title="c3">X</font> implies <font color="Maroon" title="c34">I</font> <a href="fomodel2.html#K26" title="FOMODEL2:func.26">-TruthEval</a> <font color="Maroon" title="c35">phi</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 1 )</span><br/><span class="kw">assume </span><a NAME="E1:252_1"/>
<font color="Maroon" title="c35">phi</font> <a href="hidden.html#R2" title="HIDDEN:pred.2">in</a> <font color="Maroon" title="c3">X</font>
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> <font color="Maroon" title="c34">I</font> <a href="fomodel2.html#K26" title="FOMODEL2:func.26">-TruthEval</a> <font color="Maroon" title="c35">phi</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 1</span><br/><a NAME="E2:252_1"/><span class="kw">then </span>
<font color="Maroon" title="c35">phi</font> <a href="hidden.html#R2" title="HIDDEN:pred.2">in</a> <font color="Maroon" title="c32">X22</font>
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E22:252"><span class="lab"><font color="Green" title="E145">B7</font></span></a>, <a class="ref" href="tarski.html#D3" title="TARSKI:def.3">TARSKI:def 3</a></span>;<br/><span class="kw">hence </span><a NAME="E3:252_1"/>
<font color="Maroon" title="c34">I</font> <a href="fomodel2.html#K26" title="FOMODEL2:func.26">-TruthEval</a> <font color="Maroon" title="c35">phi</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 1
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E23:252"><span class="lab"><font color="Green" title="E146">BB9</font></span></a>, <a class="ref" href="fomodel4.html#T14" target="_self" title="FOMODEL4:th.14">Th15</a>, <a class="txt" href="#E18:252"><span class="lab"><font color="Green" title="E144">B5</font></span></a>, <a class="txt" href="#E13:252"><span class="lab"><font color="Green" title="E140">B1</font></span></a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div>
<span class="kw">end;</span></div>


</div>
