let U be non empty set ; :: thesis:
let S2 be Language; :: thesis:
set FF2 = AllFormulasOf S2;
set L2 = LettersOf S2;
let X2 be countable Subset of (AllFormulasOf S2); :: thesis:
let I2 be Element of U -InterpretersOf S2; :: thesis:
assume A1: X2 is I2 -satisfied ; :: thesis:
set L = the denumerable Subset of (LettersOf S2);
reconsider SS1 = the denumerable Subset of (LettersOf S2) \/ (SymbolsOf X2) as denumerable set ;
(LettersOf S2) /\ SS1 = ( the denumerable Subset of (LettersOf S2) null (LettersOf S2)) \/ ((LettersOf S2) /\ (SymbolsOf X2)) by XBOOLE_1:23;
then consider S1 being Language such that
A2: ( OwnSymbolsOf S1 = SS1 /\ (OwnSymbolsOf S2) & S2 is S1 -extending ) by FOMODEL1:18;
( AllSymbolsOf S1 = (OwnSymbolsOf S1) \/ ((AllSymbolsOf S1) /\ {(TheEqSymbOf S1),(TheNorSymbOf S1)}) & OwnSymbolsOf S1 is countable ) by A2;
then reconsider S11 = S1 as countable Language by ORDERS_4:def 2;
reconsider S22 = S2 as S11 -extending Language by A2;
set II11 = U -InterpretersOf S11;
set II22 = U -InterpretersOf S22;
set O11 = OwnSymbolsOf S11;
set FF11 = AllFormulasOf S11;
set O22 = OwnSymbolsOf S22;
set a11 = the adicity of S11;
set a22 = the adicity of S22;
set E11 = TheEqSymbOf S11;
set E22 = TheEqSymbOf S22;
set N11 = TheNorSymbOf S11;
set N22 = TheNorSymbOf S22;
set AS11 = AtomicFormulaSymbolsOf S11;
set AS22 = AtomicFormulaSymbolsOf S22;
reconsider I22 = I2 as Element of U -InterpretersOf S22 ;
reconsider I11 = I22 | (OwnSymbolsOf S11) as Element of U -InterpretersOf S11 by FOMODEL2:2;
reconsider D11 = S11 -rules as isotone 2 -ranked Correct RuleSet of S11 ;
dom the adicity of S11 = AtomicFormulaSymbolsOf S11 by FUNCT_2:def 1;
then A3: OwnSymbolsOf S11 c= dom the adicity of S11 by FOMODEL1:1;

A4: now :: thesis:

let y be object ; :: thesis:
assume A5: y in X2 ; :: thesis:
then reconsider Y = {y} as Subset of X2 by ZFMISC_1:31;
reconsider phi2 = y as wff string of S22 by TARSKI:def 3, A5;
( SymbolsOf Y = rng phi2 & SymbolsOf Y c= SymbolsOf X2 ) by FOMODEL0:45, FOMODEL0:46;
then rng phi2 c= (SymbolsOf X2) null the denumerable Subset of (LettersOf S2) ;
then rng phi2 c= SS1 by XBOOLE_1:1;
then reconsider x = (rng phi2) /\ (OwnSymbolsOf S22) as Subset of (OwnSymbolsOf S11) by A2, XBOOLE_1:26;
( x c= dom the adicity of S11 & the adicity of S11 c= the adicity of S22 ) by A3, FOMODEL1:def 41, XBOOLE_1:1;
then A6: the adicity of S11 | x = the adicity of S22 | x by GRFUNC_1:27;
dom I11 = OwnSymbolsOf S11 by PARTFUN1:def 2;
then ( I22 | ((rng phi2) /\ (OwnSymbolsOf S22)) = I11 | ((rng phi2) /\ (OwnSymbolsOf S22)) & the adicity of S22 | ((rng phi2) /\ (OwnSymbolsOf S22)) = the adicity of S11 | ((rng phi2) /\ (OwnSymbolsOf S22)) & TheEqSymbOf S11 = TheEqSymbOf S22 & TheNorSymbOf S11 = TheNorSymbOf S22 ) by FOMODEL1:def 41, A6, GRFUNC_1:27;
then consider phi1 being wff string of S11 such that
A7: phi2 = phi1 by FOMODEL3:16;
thus y in AllFormulasOf S11 by FOMODEL2:16, A7; :: thesis:

end;

now :: thesis:

let phi1 be wff string of S11; :: thesis:
( OwnSymbolsOf S11 c= AtomicFormulaSymbolsOf S11 & dom the adicity of S11 = AtomicFormulaSymbolsOf S11 ) by FOMODEL1:1, FUNCT_2:def 1;
then ( TheNorSymbOf S11 = TheNorSymbOf S22 & TheEqSymbOf S11 = TheEqSymbOf S22 & I11 | (OwnSymbolsOf S11) = I22 | (OwnSymbolsOf S11) & the adicity of S11 | (OwnSymbolsOf S11) = the adicity of S22 | (OwnSymbolsOf S11) ) by GRFUNC_1:27, FOMODEL1:def 41;
then consider phi2 being wff string of S22 such that
A8: ( phi2 = phi1 & I22 -TruthEval phi2 = I11 -TruthEval phi1 ) by FOMODEL3:12;
assume phi1 in X2 ; :: thesis:
hence 1 = I11 -TruthEval phi1 by A8, A1; :: thesis:

end;

now :: thesis:

let phi be wff string of S22; :: thesis:
assume A12: phi in X2 ; :: thesis:
then phi in AllFormulasOf S11 by A4;
then reconsider phi1 = phi as wff string of S11 ;
consider phi2 being wff string of S22 such that
A13: ( phi1 = phi2 & I1 -TruthEval phi1 = IT -TruthEval phi2 ) by A10, A11, FOMODEL3:12;
thus 1 = IT -TruthEval phi by A13, A12, A9; :: thesis:

end;

hence X2 is ITT -satisfied ; :: thesis: