let S be Language; :: thesis: R#4 S is Correct

now :: thesis: for X being set st X is S -correct holds
(R#4 S) . X is S -correct

set f = R#4 S;
set R = P#4 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 ;
let X be set ; :: thesis: ( X is S -correct implies (R#4 S) . X is S -correct )
assume A1: X is S -correct ; :: thesis: (R#4 S) . X is S -correct

now :: thesis: for U being non empty set
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 (R#4 S) . X holds
I -TruthEval psi = 1

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 (R#4 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 (R#4 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 (R#4 S) . X holds
I -TruthEval psi = 1
let psi be wff string of S; :: thesis: ( [x,psi] in (R#4 S) . X implies I -TruthEval psi = 1 )
set s = [x,psi];
assume A3: [x,psi] in (R#4 S) . X ; :: thesis: I -TruthEval psi = 1
then A4: ( [x,psi] in S -sequents & [X,[x,psi]] in P#4 S ) by Lm30;
then X in dom (P#4 S) by XTUPLE_0:def 12;
then reconsider Seqts = X as S -correct Subset of (S -sequents) by A1;
reconsider seqt = [x,psi] as Element of S -sequents by A3, Lm30;
seqt Rule4 Seqts by A4, Def41;
then consider l being literal Element of S, phi being wff string of S, t being termal string of S such that
A5: ( seqt `1 = {((l,t) SubstIn phi)} & seqt `2 = <*l*> ^ phi ) ;
reconsider tt = t as Element of AllTermsOf S by FOMODEL1:def 32;
reconsider phii = (l,tt) SubstIn phi as wff string of S ;
reconsider u = (I -TermEval) . tt as Element of U ;
reconsider I1 = (l,u) ReassignIn I as Element of U -InterpretersOf S ;
A6: ( x = {phii} & psi = <*l*> ^ phi ) by A5;
then 1 = I -TruthEval phii by FOMODEL2:27
.= I1 -TruthEval phi by FOMODEL3:10 ;
hence I -TruthEval psi = 1 by A6, FOMODEL2:19; :: thesis: verum

end;

hence (R#4 S) . X is S -correct ; :: thesis: verum

end;

hence R#4 S is Correct ; :: thesis: verum