let S be Language; :: thesis: R#3a S is Correct

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

set f = R#3a S;
set R = P#3a 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 (R#3a S) . X is S -correct )
assume A1: X is S -correct ; :: thesis: (R#3a 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#3a 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#3a 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#3a 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#3a S) . X holds
I -TruthEval psi = 1
let psi be wff string of S; :: thesis: ( [x,psi] in (R#3a S) . X implies I -TruthEval psi = 1 )
set s = [x,psi];
set TE = I -TermEval ;
set d = U -deltaInterpreter ;
A2: ( ([x,psi] `1) \+\ x = {} & ([x,psi] `2) \+\ psi = {} ) ;
assume A3: [x,psi] in (R#3a S) . X ; :: thesis: I -TruthEval psi = 1
then A4: ( [x,psi] in S -sequents & [X,[x,psi]] in P#3a S ) by Lm29;
then X in dom (P#3a 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, Lm29;
seqt Rule3a Seqts by A4, Def34;
then consider t, t1, t2 being termal string of S, y being set such that
A5: ( y in Seqts & seqt `1 = (y `1) \/ {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} & y `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t1 & seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t2 ) by Def21;
reconsider phi1 = (<*(TheEqSymbOf S)*> ^ t) ^ t1, phi2 = (<*(TheEqSymbOf S)*> ^ t) ^ t2, phi = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 as 0wff string of S ;
reconsider gamma = (y `1) null {phi}, z = {phi} null (y `1) as Subset of x by A5, A2;
[gamma,phi1] in Seqts by A5, MCART_1:21;
then I -TruthEval phi1 = 1 by FOMODEL2:def 44;
then A6: ( phi2 = psi & (I -TermEval) . t = (I -TermEval) . t1 ) by Lm57, A2, A5;
z = {phi} ;
then I -TruthEval phi = 1 by FOMODEL2:27;
then (I -TermEval) . t2 = (I -TermEval) . t by A6, Lm57;
then I -AtomicEval phi2 = 1 by Lm57;
hence I -TruthEval psi = 1 by A2, A5; :: thesis: verum

end;

hence (R#3a S) . X is S -correct by FOMODEL2:def 44; :: thesis: verum

end;

hence R#3a S is Correct by Def69; :: thesis: verum