let S be Language; :: thesis: for D2 being 2 -ranked RuleSet of S
for X being functional set st AllFormulasOf S is countable & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & not X is D2 -inconsistent & D2 is isotone holds
ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied
let D2 be 2 -ranked RuleSet of S; :: thesis: for X being functional set st AllFormulasOf S is countable & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & not X is D2 -inconsistent & D2 is isotone holds
ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied
let X be functional set ; :: thesis: ( AllFormulasOf S is countable & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & not X is D2 -inconsistent & D2 is isotone implies ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied )
set EF = ExFormulasOf S;
set FF = AllFormulasOf S;
set G0 = R0 S;
set G2 = R2 S;
set G3a = R3a S;
set G3b = R3b S;
set G3d = R3d S;
set G3e = R3e S;
set G1 = R1 S;
set G4 = R4 S;
set G5 = R5 S;
set G6 = R6 S;
set G7 = R7 S;
set G8 = R8 S;
set L = LettersOf S;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set no = SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}));
set D = D2;
reconsider D1 = D2 as 0 -ranked 1 -ranked RuleSet of S ;
assume AllFormulasOf S is countable ; :: thesis: ( (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite or X is D2 -inconsistent or not D2 is isotone or ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied )
then reconsider FFC = AllFormulasOf S as countable set ;
consider numaa being Function of NAT,(((AllSymbolsOf S) *) \ {{}}) such that
B10: FFC = rng numaa by SUPINF_2:def 8;
reconsider numa = numaa as Function of NAT,(AllFormulasOf S) by B10, FUNCT_2:6;
(ExFormulasOf S) \ FFC = {} ;
then reconsider EFC = ExFormulasOf S as Subset of FFC by XBOOLE_1:37;
consider numee being Function of NAT,FFC such that
B6: EFC = rng numee by SUPINF_2:def 8;
reconsider nume = numee as Function of NAT,(ExFormulasOf S) by B6, FUNCT_2:6;
assume B0: ( not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & not X is D2 -inconsistent ) ; :: thesis: ( not D2 is isotone or ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied )
B1: ( R0 S in D1 & R1 S in D2 & R2 S in D1 & R4 S in D2 & R5 S in D2 & R6 S in D2 & R7 S in D2 & R8 S in D2 ) by DefRank;
set X1 = X addw (D1,nume);
set X2 = (D1,numa) CompletionOf (X addw (D1,nume));
B3: (D1,numa) CompletionOf (X addw (D1,nume)) is S -covering by Lm5, B10;
assume B2: D2 is isotone ; :: thesis: ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied
then not X addw (D1,nume) is D2 -inconsistent by Lm6, B0, B1;
then B4: not (D1,numa) CompletionOf (X addw (D1,nume)) is D2 -inconsistent by Lm7, B2, B1;
then B5: ( (D1,numa) CompletionOf (X addw (D1,nume)) is S -mincover & (D1,numa) CompletionOf (X addw (D1,nume)) is D2 -expanded ) by B1, Lm8, B3;
reconsider X22 = (D1,numa) CompletionOf (X addw (D1,nume)) as D1 -expanded set by B1, Lm8, B3, B4;
take U = Class ((X22,D1) -termEq); :: thesis: ex I being Element of U -InterpretersOf S st X is I -satisfied
reconsider I = D1 Henkin X22 as Element of U -InterpretersOf S ;
take I ; :: thesis: X is I -satisfied
( X \ (X addw (D1,nume)) = {} & (X addw (D1,nume)) \ ((D1,numa) CompletionOf (X addw (D1,nume))) = {} ) ;
then B7: ( X c= X addw (D1,nume) & X addw (D1,nume) c= X22 ) by XBOOLE_1:37;
then BB9: X22 is S -witnessed by Th19, B0, B1, B2, B4, B6;

hereby :: according to FOMODEL2:def 42 :: thesis: verum

let phi be wff string of S; :: thesis: ( phi in X implies I -TruthEval phi = 1 )
assume phi in X ; :: thesis: I -TruthEval phi = 1
then phi in X22 by B7, TARSKI:def 3;
hence I -TruthEval phi = 1 by BB9, Th15, B5, B1; :: thesis: verum

end;