let X be set ; :: thesis: for U being non empty 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 U be non empty 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 FUNCT_2:def 1, FOMODEL1: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 A1: 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 | (OwnSymbolsOf S1) = ( the adicity of S2 | (dom the adicity of S1)) | (OwnSymbolsOf S1) by GRFUNC_1:34

.= the adicity of S2 | (O11 null (dom the adicity of S1)) by RELAT_1:71 ;

then A2: ( the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) & TheNorSymbOf S1 = TheNorSymbOf S2 & TheEqSymbOf S1 = TheEqSymbOf S2 ) by A1;

assume A3: ( X c= AllFormulasOf S1 & I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) ) ; :: thesis: ( X is I1 -satisfied iff X is I2 -satisfied )

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 U be non empty 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 FUNCT_2:def 1, FOMODEL1: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 A1: 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 | (OwnSymbolsOf S1) = ( the adicity of S2 | (dom the adicity of S1)) | (OwnSymbolsOf S1) by GRFUNC_1:34

.= the adicity of S2 | (O11 null (dom the adicity of S1)) by RELAT_1:71 ;

then A2: ( the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) & TheNorSymbOf S1 = TheNorSymbOf S2 & TheEqSymbOf S1 = TheEqSymbOf S2 ) by A1;

assume A3: ( 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 A7:
X is I2 -satisfied
; :: thesis: X is I1 -satisfied assume A4:
X is I1 -satisfied
; :: thesis: X is I2 -satisfied

end;now :: thesis: for phi2 being wff string of S2 st phi2 in X holds

I2 -TruthEval phi2 = 1

hence
X is I2 -satisfied
; :: thesis: verumI2 -TruthEval phi2 = 1

let phi2 be wff string of S2; :: thesis: ( phi2 in X implies I2 -TruthEval phi2 = 1 )

assume A5: phi2 in X ; :: thesis: I2 -TruthEval phi2 = 1

then phi2 in AllFormulasOf S1 by A3;

then reconsider phi1 = phi2 as wff string of S1 ;

consider phi22 being wff string of S2 such that

A6: ( phi1 = phi22 & I1 -TruthEval phi1 = I2 -TruthEval phi22 ) by Th12, A2, A3;

thus I2 -TruthEval phi2 = 1 by A6, A5, A4; :: thesis: verum

end;assume A5: phi2 in X ; :: thesis: I2 -TruthEval phi2 = 1

then phi2 in AllFormulasOf S1 by A3;

then reconsider phi1 = phi2 as wff string of S1 ;

consider phi22 being wff string of S2 such that

A6: ( phi1 = phi22 & I1 -TruthEval phi1 = I2 -TruthEval phi22 ) by Th12, A2, A3;

thus I2 -TruthEval phi2 = 1 by A6, A5, A4; :: thesis: verum

now :: thesis: for phi1 being wff string of S1 st phi1 in X holds

I1 -TruthEval phi1 = 1

hence
X is I1 -satisfied
; :: thesis: verumI1 -TruthEval phi1 = 1

let phi1 be wff string of S1; :: thesis: ( phi1 in X implies I1 -TruthEval phi1 = 1 )

assume A8: phi1 in X ; :: thesis: I1 -TruthEval phi1 = 1

consider phi2 being wff string of S2 such that

A9: ( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 ) by Th12, A2, A3;

thus I1 -TruthEval phi1 = 1 by A9, A8, A7; :: thesis: verum

end;assume A8: phi1 in X ; :: thesis: I1 -TruthEval phi1 = 1

consider phi2 being wff string of S2 such that

A9: ( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 ) by Th12, A2, A3;

thus I1 -TruthEval phi1 = 1 by A9, A8, A7; :: thesis: verum