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 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 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 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;
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 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
A1: FFC = rng numaa by SUPINF_2:def 8;
reconsider numa = numaa as Function of NAT,(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 Function of NAT,FFC such that
A2: EFC = rng numee by SUPINF_2:def 8;
reconsider nume = numee as Function of NAT,(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 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 Def59;
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 Lm73, A1;
assume A6: D2 is isotone ; :: thesis: ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied
then X addw (D1,nume) is D2 -consistent by Lm71, 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, Lm54, A5;
reconsider X22 = (D1,numa) CompletionOf (X addw (D1,nume)) as D1 -expanded set by A4, Lm54, A5, A7;
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 A9: ( X c= X addw (D1,nume) & X addw (D1,nume) c= X22 ) by XBOOLE_1:37;
then A10: X22 is S -witnessed by 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 A9, TARSKI:def 3;
hence I -TruthEval phi = 1 by A10, Th14, A8, A4; :: thesis: verum

end;