let U be non empty set ; :: thesis: for X being set
for S being Language
for D being RuleSet of S
for I being Element of U -InterpretersOf S st D is Correct & X is I -satisfied holds
X is D -consistent
let X be set ; :: thesis: for S being Language
for D being RuleSet of S
for I being Element of U -InterpretersOf S st D is Correct & X is I -satisfied holds
X is D -consistent
let S be Language; :: thesis: for D being RuleSet of S
for I being Element of U -InterpretersOf S st D is Correct & X is I -satisfied holds
X is D -consistent
let D be RuleSet of S; :: thesis: for I being Element of U -InterpretersOf S st D is Correct & X is I -satisfied holds
X is D -consistent
set N = TheNorSymbOf S;
let I be Element of U -InterpretersOf S; :: thesis: ( D is Correct & X is I -satisfied implies X is D -consistent )
assume A1: ( D is Correct & X is I -satisfied ) ; :: thesis: X is D -consistent

now :: thesis: for phi1, phi2 being wff string of S holds
( not phi1 is X,D -provable or not (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable )

given phi1, phi2 being wff string of S such that A2: ( phi1 is X,D -provable & (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable ) ; :: thesis: contradiction
set nphi1 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
( I -TruthEval phi1 = 1 & I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = 1 ) by A2, A1;
hence contradiction by FOMODEL2:19; :: thesis: verum

end;

hence X is D -consistent ; :: thesis: verum