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 )
hereby :: thesis: ( X is I2 -satisfied implies X is I1 -satisfied )
assume A4: X is I1 -satisfied ; :: thesis: X is I2 -satisfied
now :: thesis: for phi2 being wff string of S2 st phi2 in X holds
I2 -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;
hence X is I2 -satisfied ; :: thesis: verum
end;
assume A7: X is I2 -satisfied ; :: thesis: X is I1 -satisfied
now :: thesis: for phi1 being wff string of S1 st phi1 in X holds
I1 -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;
hence X is I1 -satisfied ; :: thesis: verum