let U be non empty set ; :: thesis: for X being set
for S1, S2 being Language
for I1 being Element of U -InterpretersOf S1
for I2 being Element of U -InterpretersOf S2 st S2 is S1 -extending & X c= AllFormulasOf S1 & I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds
( X is I1 -satisfied iff X is I2 -satisfied )
let X be set ; :: thesis: for S1, S2 being Language
for I1 being Element of U -InterpretersOf S1
for I2 being Element of U -InterpretersOf S2 st S2 is S1 -extending & X c= AllFormulasOf S1 & I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds
( X is I1 -satisfied iff X is I2 -satisfied )
let S1, S2 be Language; :: thesis: for I1 being Element of U -InterpretersOf S1
for I2 being Element of U -InterpretersOf S2 st S2 is S1 -extending & X c= AllFormulasOf S1 & I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds
( X is I1 -satisfied iff X is I2 -satisfied )
set II1 = U -InterpretersOf S1;
set II2 = U -InterpretersOf S2;
set a1 = the adicity of S1;
set a2 = the adicity of S2;
set O1 = OwnSymbolsOf S1;
set E1 = TheEqSymbOf S1;
set E2 = TheEqSymbOf S2;
set N1 = TheNorSymbOf S1;
set N2 = TheNorSymbOf S2;
set FF1 = AllFormulasOf S1;
set AS1 = AtomicFormulaSymbolsOf S1;
( dom the adicity of S1 = AtomicFormulaSymbolsOf S1 & OwnSymbolsOf S1 c= AtomicFormulaSymbolsOf S1 ) by FOMODEL1:1, FUNCT_2:def 1;
then reconsider O11 = OwnSymbolsOf S1 as Subset of (dom the adicity of S1) ;
let I1 be Element of U -InterpretersOf S1; :: thesis: for I2 being Element of U -InterpretersOf S2 st S2 is S1 -extending & X c= AllFormulasOf S1 & I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds
( X is I1 -satisfied iff X is I2 -satisfied )
let I2 be Element of U -InterpretersOf S2; :: thesis: ( S2 is S1 -extending & X c= AllFormulasOf S1 & I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) implies ( X is I1 -satisfied iff X is I2 -satisfied ) )
assume B5: S2 is S1 -extending ; :: thesis: ( not X c= AllFormulasOf S1 or not I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) or ( X is I1 -satisfied iff X is I2 -satisfied ) )
then the adicity of S1 c= the adicity of S2 by FOMODEL1:def 41;
then the adicity of S1 | (OwnSymbolsOf S1) = ( the adicity of S2 | (dom the adicity of S1)) | (OwnSymbolsOf S1) by GRFUNC_1:23
.= the adicity of S2 | (O11 null (dom the adicity of S1)) by RELAT_1:71 ;
then B1: ( the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) & TheNorSymbOf S1 = TheNorSymbOf S2 & TheEqSymbOf S1 = TheEqSymbOf S2 ) by B5, FOMODEL1:def 41;
assume B2: ( X c= AllFormulasOf S1 & I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) ) ; :: thesis: ( X is I1 -satisfied iff X is I2 -satisfied )

hereby :: thesis: ( X is I2 -satisfied implies X is I1 -satisfied )

assume B3: X is I1 -satisfied ; :: thesis: X is I2 -satisfied

now

let phi2 be wff string of S2; :: thesis: ( phi2 in X implies I2 -TruthEval phi2 = 1 )
assume C0: phi2 in X ; :: thesis: I2 -TruthEval phi2 = 1
then phi2 in AllFormulasOf S1 by B2;
then reconsider phi1 = phi2 as wff string of S1 ;
consider phi22 being wff string of S2 such that
C1: ( phi1 = phi22 & I1 -TruthEval phi1 = I2 -TruthEval phi22 ) by B1, B2, FOMODEL3:12;
thus I2 -TruthEval phi2 = 1 by C1, C0, B3, FOMODEL2:def 42; :: thesis: verum

end;

hence X is I2 -satisfied by FOMODEL2:def 42; :: thesis: verum

end;

assume B4: X is I2 -satisfied ; :: thesis: X is I1 -satisfied

now

let phi1 be wff string of S1; :: thesis: ( phi1 in X implies I1 -TruthEval phi1 = 1 )
assume C0: phi1 in X ; :: thesis: I1 -TruthEval phi1 = 1
consider phi2 being wff string of S2 such that
C1: ( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 ) by B1, B2, FOMODEL3:12;
thus I1 -TruthEval phi1 = 1 by C1, C0, B4, FOMODEL2:def 42; :: thesis: verum

end;

hence X is I1 -satisfied by FOMODEL2:def 42; :: thesis: verum