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
not X is D -inconsistent
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
not X is D -inconsistent
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
not X is D -inconsistent
let D be RuleSet of S; :: thesis: for I being Element of U -InterpretersOf S st D is Correct & X is I -satisfied holds
not X is D -inconsistent
set N = TheNorSymbOf S;
let I be Element of U -InterpretersOf S; :: thesis: ( D is Correct & X is I -satisfied implies not X is D -inconsistent )
assume B0: ( D is Correct & X is I -satisfied ) ; :: thesis: not X is D -inconsistent

now

given phi1, phi2 being wff string of S such that C0: ( 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 C0, B0, DefCorrect;
hence contradiction by FOMODEL2:19; :: thesis: verum

end;

hence not X is D -inconsistent by DefInc; :: thesis: verum