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

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

set f = R#8 S;
set R = P#8 S;
set Q = S -sequents ;
set E = TheEqSymbOf S;
set N = TheNorSymbOf S;
let X be set ; :: thesis: ( X is S -correct implies (R#8 S) . X is S -correct )
assume A1: X is S -correct ; :: thesis: (R#8 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#8 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#8 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#8 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#8 S) . X holds
I -TruthEval psi = 1
let psi be wff string of S; :: thesis: ( [x,psi] in (R#8 S) . X implies I -TruthEval psi = 1 )
set s = [x,psi];
assume A3: [x,psi] in (R#8 S) . X ; :: thesis: I -TruthEval psi = 1
then A4: ( [x,psi] in S -sequents & [X,[x,psi]] in P#8 S ) by Lm30;
then X in dom (P#8 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 Rule8 Seqts by A4, Def45;
then consider y1, y2 being set , phi, phi1, phi2 being wff string of S such that
A5: ( y1 in Seqts & y2 in Seqts & y1 `1 = y2 `1 & y1 `2 = phi1 & y2 `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & {phi} \/ (seqt `1) = y1 `1 & seqt `2 = (<*(TheNorSymbOf S)*> ^ phi) ^ phi ) ;
reconsider Seqts = Seqts as non empty Subset of (S -sequents) by A5;
reconsider seqt1 = y1, seqt2 = y2 as Element of Seqts by A5;
reconsider H = seqt1 `1 as S -premises-like set ;
A6: ( {phi} \/ x = H & psi = (<*(TheNorSymbOf S)*> ^ phi) ^ phi ) by A5;

now :: thesis: not I -TruthEval phi = 1

assume I -TruthEval phi = 1 ; :: thesis: contradiction
then reconsider H1 = {phi} as I -satisfied set by FOMODEL2:27;
H1 \/ x is I -satisfied ;
then reconsider H2 = H as I -satisfied set by A5;
( [H2,phi1] in Seqts & [H2,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] in Seqts ) by A5, MCART_1:21;
then ( I -TruthEval phi1 = 1 & I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = 1 ) by FOMODEL2:def 44;
hence contradiction by FOMODEL2:19; :: thesis: verum

end;

then I -TruthEval phi = 0 by FOMODEL0:39;
hence I -TruthEval psi = 1 by A6, FOMODEL2:19; :: thesis: verum

end;

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

end;

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