let S be Language; :: thesis: R0 S is Correct

now

set f = R0 S;
set R = P0 S;
set Q = S -sequents ;
let X be set ; :: thesis: ( X is S -correct implies (R0 S) . X is S -correct )
assume X is S -correct ; :: thesis: (R0 S) . X is S -correct

now

let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S
for x being b₁ -satisfied set
for phi being wff string of S st [x,phi] in (R0 S) . X holds
I -TruthEval phi = 1
set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: for x being I -satisfied set
for phi being wff string of S st [x,phi] in (R0 S) . X holds
I -TruthEval phi = 1
let x be I -satisfied set ; :: thesis: for phi being wff string of S st [x,phi] in (R0 S) . X holds
I -TruthEval phi = 1
let phi be wff string of S; :: thesis: ( [x,phi] in (R0 S) . X implies I -TruthEval phi = 1 )
set s = [x,phi];
( ([x,phi] `1) \+\ x = {} & ([x,phi] `2) \+\ phi = {} ) ;
then C0: ( dom (P0 S) c= bool (S -sequents) & [x,phi] `1 = x & [x,phi] `2 = phi ) by FOMODEL0:29;
assume DD1: [x,phi] in (R0 S) . X ; :: thesis: I -TruthEval phi = 1
then D1: ( [x,phi] in S -sequents & [X,[x,phi]] in P0 S ) by Lm1e;
then X in dom (P0 S) by RELAT_1:def 4;
then reconsider XX = X as Subset of (S -sequents) ;
reconsider seqt = [x,phi] as Element of S -sequents by DD1, Lm1e;
seqt Rule0 XX by D1, DefP0;
then phi in x by C0, Def0;
hence I -TruthEval phi = 1 by FOMODEL2:def 42; :: thesis: verum

end;

hence (R0 S) . X is S -correct by FOMODEL2:def 44; :: thesis: verum

end;

hence R0 S is Correct by RuleCorr; :: thesis: verum