let S be Language; :: thesis: for D2 being 2 -ranked RuleSet of S
for X being functional set st AllFormulasOf S is countable & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D2 -consistent & D2 is isotone holds
ex U being non empty countable 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 & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D2 -consistent & D2 is isotone holds
ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied
let X be functional set ; :: thesis: ( AllFormulasOf S is countable & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D2 -consistent & D2 is isotone implies ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied )
set EF = ExFormulasOf S;
set FF = AllFormulasOf S;
set G0 = R#0 S;
set G2 = R#2 S;
set G3a = R#3a S;
set G3b = R#3b S;
set G3d = R#3d S;
set G3e = R#3e S;
set G1 = R#1 S;
set G4 = R#4 S;
set G5 = R#5 S;
set G6 = R#6 S;
set G7 = R#7 S;
set G8 = R#8 S;
set L = LettersOf S;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set no = SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}));
set D = D2;
set AF = AtomicFormulasOf S;
set TT = AllTermsOf S;
set d = S -diagFormula ;
D2 is 1 -ranked RuleSet of S ;
then D2 is 0 -ranked RuleSet of S ;
then reconsider D1 = D2 as 0 -ranked 1 -ranked RuleSet of S ;
assume AllFormulasOf S is countable ; :: thesis: ( not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite or not X is D2 -consistent or not D2 is isotone or ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied )
then reconsider FFC = AllFormulasOf S as countable set ;
(AtomicFormulasOf S) \ (AllFormulasOf S) = {} ;
then reconsider AFF = AtomicFormulasOf S as Subset of FFC by XBOOLE_1:37;
( dom (S -diagFormula) = AllTermsOf S & rng (S -diagFormula) c= AtomicFormulasOf S ) by FUNCT_2:def 1, RELAT_1:def 19;
then card (AllTermsOf S) c= card AFF by CARD_1:10;
then reconsider TTT = AllTermsOf S as non empty countable Subset of (((AllSymbolsOf S) *) \ {{}}) by WAYBEL12:1;
consider numaa being sequence of (((AllSymbolsOf S) *) \ {{}}) such that
A1: FFC = rng numaa by SUPINF_2:def 8;
reconsider numa = numaa as sequence of (AllFormulasOf S) by A1, FUNCT_2:6;
(ExFormulasOf S) \ FFC = {} ;
then reconsider EFC = ExFormulasOf S as Subset of FFC by XBOOLE_1:37;
consider numee being sequence of FFC such that
A2: EFC = rng numee by SUPINF_2:def 8;
reconsider nume = numee as sequence of (ExFormulasOf S) by A2, FUNCT_2:6;
assume A3: ( (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D2 -consistent ) ; :: thesis: ( not D2 is isotone or ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied )
A4: ( R#0 S in D1 & R#1 S in D2 & R#2 S in D1 & R#4 S in D2 & R#5 S in D2 & R#6 S in D2 & R#7 S in D2 & R#8 S in D2 ) by Def62;
set X1 = X addw (D1,nume);
set X2 = (D1,numa) CompletionOf (X addw (D1,nume));
A5: (D1,numa) CompletionOf (X addw (D1,nume)) is S -covering by Lm69, A1;
assume A6: D2 is isotone ; :: thesis: ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied
then X addw (D1,nume) is D2 -consistent by Lm68, A3, A4;
then A7: (D1,numa) CompletionOf (X addw (D1,nume)) is D2 -consistent by Lm74, A6, A4;
then A8: ( (D1,numa) CompletionOf (X addw (D1,nume)) is S -mincover & (D1,numa) CompletionOf (X addw (D1,nume)) is D2 -expanded ) by A4, Lm52, A5;
reconsider X22 = (D1,numa) CompletionOf (X addw (D1,nume)) as D1 -expanded set by A4, Lm52, A5, A7;
reconsider P = (X22,D1) -termEq as Equivalence_Relation of TTT ;
set f = P -class ;
( dom (P -class) = TTT & rng (P -class) = Class P ) by FUNCT_2:def 1, FUNCT_2:def 3;
then card (Class P) c= card TTT by CARD_1:12;
then reconsider U = Class P as non empty countable set by WAYBEL12:1;
take U ; :: 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
A9: ( X \ (X addw (D1,nume)) = {} & (X addw (D1,nume)) \ ((D1,numa) CompletionOf (X addw (D1,nume))) = {} ) ;
then A10: ( X c= X addw (D1,nume) & X addw (D1,nume) c= X22 ) by XBOOLE_1:37;
A11: X22 is S -witnessed by A9, XBOOLE_1:37, Th18, A3, A4, A6, A7, A2;

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 TARSKI:def 3, A10;
hence I -TruthEval phi = 1 by A11, Th16, A8, A4; :: thesis: verum

end;