let Z be set ; :: thesis: for S being countable Language
for D being RuleSet of S st D is 2 -ranked & D is isotone & D is Correct & Z is D -consistent & Z c= AllFormulasOf S holds
ex U being non empty countable set ex I being Element of U -InterpretersOf S st Z is I -satisfied
let S be countable Language; :: thesis: for D being RuleSet of S st D is 2 -ranked & D is isotone & D is Correct & Z is D -consistent & Z c= AllFormulasOf S holds
ex U being non empty countable set ex I being Element of U -InterpretersOf S st Z is I -satisfied
set S1 = S;
let D be RuleSet of S; :: thesis: ( D is 2 -ranked & D is isotone & D is Correct & Z is D -consistent & Z c= AllFormulasOf S implies ex U being non empty countable set ex I being Element of U -InterpretersOf S st Z is I -satisfied )
set FF1 = AllFormulasOf S;
assume A1: ( D is 2 -ranked & D is isotone & D is Correct & Z is D -consistent & Z c= AllFormulasOf S ) ; :: thesis: ex U being non empty countable set ex I being Element of U -InterpretersOf S st Z is I -satisfied
then reconsider X = Z as Subset of (AllFormulasOf S) ;
set S2 = S addLettersNotIn X;
set O1 = OwnSymbolsOf S;
set O2 = OwnSymbolsOf (S addLettersNotIn X);
set FF2 = AllFormulasOf (S addLettersNotIn X);
set SS1 = AllSymbolsOf S;
set SS2 = AllSymbolsOf (S addLettersNotIn X);
set strings2 = ((AllSymbolsOf (S addLettersNotIn X)) *) \ {{}};
set L2 = LettersOf (S addLettersNotIn X);
reconsider D1 = D as 2 -ranked Correct RuleSet of S by A1;
(OwnSymbolsOf S) \ (OwnSymbolsOf (S addLettersNotIn X)) = {} ;
then reconsider O11 = OwnSymbolsOf S as non empty Subset of (OwnSymbolsOf (S addLettersNotIn X)) by XBOOLE_1:37;
reconsider D2 = (S addLettersNotIn X) -rules as isotone 2 -ranked Correct RuleSet of (S addLettersNotIn X) ;
reconsider sub1 = X /\ (((AllSymbolsOf (S addLettersNotIn X)) *) \ {{}}) as Subset of X ;
reconsider sub2 = SymbolsOf sub1 as Subset of (SymbolsOf X) by FOMODEL0:46;
reconsider inf = (LettersOf (S addLettersNotIn X)) \ (SymbolsOf X) as Subset of ((LettersOf (S addLettersNotIn X)) \ sub2) by XBOOLE_1:34;
A2: (LettersOf (S addLettersNotIn X)) \ (sub2 null inf) is infinite ;

now :: thesis: for Y being finite Subset of X holds Y is D2 -consistent

let Y be finite Subset of X; :: thesis: Y is D2 -consistent
reconsider YY = Y as functional set ;
reconsider YYY = YY as functional Subset of (AllFormulasOf S) by XBOOLE_1:1;
( YY is finite & AllFormulasOf S is countable & YY is D1 -consistent & D1 is isotone ) by A1;
then consider U being non empty countable set such that
A3: ex I1 being Element of U -InterpretersOf S st YY is I1 -satisfied by Lm76;
set II1 = U -InterpretersOf S;
set II2 = U -InterpretersOf (S addLettersNotIn X);
set I02 = the S addLettersNotIn X,U -interpreter-like Function;
consider I1 being Element of U -InterpretersOf S such that
A4: YYY is I1 -satisfied by A3;
reconsider I2 = ( the S addLettersNotIn X,U -interpreter-like Function +* I1) | (OwnSymbolsOf (S addLettersNotIn X)) as Element of U -InterpretersOf (S addLettersNotIn X) by FOMODEL2:2;
I2 | (OwnSymbolsOf S) = ( the S addLettersNotIn X,U -interpreter-like Function +* I1) | (O11 null (OwnSymbolsOf (S addLettersNotIn X))) by RELAT_1:71
.= ( the S addLettersNotIn X,U -interpreter-like Function | (OwnSymbolsOf S)) +* (I1 | (OwnSymbolsOf S)) by FUNCT_4:71
.= I1 | (OwnSymbolsOf S) ;
then YYY is I2 -satisfied by A4, FOMODEL3:17;
hence Y is D2 -consistent by Lm53; :: thesis: verum

end;

then X is D2 -consistent by Lm51;
then consider U being non empty countable set , I2 being Element of U -InterpretersOf (S addLettersNotIn X) such that
A5: X is I2 -satisfied by A2, Lm75;
set II1 = U -InterpretersOf S;
set II2 = U -InterpretersOf (S addLettersNotIn X);
take U ; :: thesis: ex I being Element of U -InterpretersOf S st Z is I -satisfied
reconsider I1 = I2 | (OwnSymbolsOf S) as Element of U -InterpretersOf S by FOMODEL2:2;
take I1 ; :: thesis: Z is I1 -satisfied
I1 | (OwnSymbolsOf S) = (I2 | (OwnSymbolsOf S)) null (OwnSymbolsOf S) ;
hence Z is I1 -satisfied by A5, FOMODEL3:17; :: thesis: verum