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

now

set f = R3b S;
set R = P3b S;
set Q = S -sequents ;
set E = TheEqSymbOf S;
set N = TheNorSymbOf S;
set FF = AllFormulasOf S;
set TT = AllTermsOf S;
set SS = AllSymbolsOf S;
set F = S -firstChar ;
set C = S -multiCat ;
let X be set ; :: thesis: ( X is S -correct implies (R3b S) . X is S -correct )
assume B0: X is S -correct ; :: thesis: (R3b 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 psi being wff string of S st [x,psi] in (R3b S) . X holds
I -TruthEval psi = 1
set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: for x being I -satisfied set
for psi being wff string of S st [x,psi] in (R3b S) . X holds
I -TruthEval psi = 1
let x be I -satisfied set ; :: thesis: for psi being wff string of S st [x,psi] in (R3b S) . X holds
I -TruthEval psi = 1
let psi be wff string of S; :: thesis: ( [x,psi] in (R3b S) . X implies I -TruthEval psi = 1 )
set s = [x,psi];
set TE = I -TermEval ;
set d = U -deltaInterpreter ;
CC0: ( ([x,psi] `1) \+\ x = {} & ([x,psi] `2) \+\ psi = {} ) ;
assume DD1: [x,psi] in (R3b S) . X ; :: thesis: I -TruthEval psi = 1
then D1: ( [x,psi] in S -sequents & [X,[x,psi]] in P3b S ) by Lm1e;
then X in dom (P3b S) by RELAT_1:def 4;
then reconsider Seqts = X as S -correct Subset of (S -sequents) by B0;
reconsider seqt = [x,psi] as Element of S -sequents by DD1, Lm1e;
seqt Rule3b Seqts by D1, DefP3b;
then consider t1, t2 being termal string of S such that
D2: ( seqt `1 = {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} & seqt `2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t1 ) by Def3b;
set phi1 = (<*(TheEqSymbOf S)*> ^ t1) ^ t2;
set phi2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t1;
{((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} is I -satisfied by D2, CC0, FOMODEL0:29;
then 1 = I -AtomicEval ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) by FOMODEL2:27;
then (I -TermEval) . t1 = (I -TermEval) . t2 by Lm36;
then ( I -AtomicEval ((<*(TheEqSymbOf S)*> ^ t2) ^ t1) = 1 & (<*(TheEqSymbOf S)*> ^ t2) ^ t1 = psi ) by D2, CC0, Lm36, FOMODEL0:29;
hence I -TruthEval psi = 1 ; :: thesis: verum

end;

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

end;

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