let S be Language; R3e S is Correct
now set f =
R3e S;
set R =
P3e 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 ;
( X is S -correct implies (R3e S) . X is S -correct )assume B0:
X is
S -correct
;
(R3e S) . X is S -correct now let U be non
empty set ;
for I being Element of U -InterpretersOf S
for x being b1 -satisfied set
for psi being wff string of S st [x,psi] in (R3e S) . X holds
b5 -TruthEval b7 = 1set II =
U -InterpretersOf S;
let I be
Element of
U -InterpretersOf S;
for x being I -satisfied set
for psi being wff string of S st [x,psi] in (R3e S) . X holds
b4 -TruthEval b6 = 1let x be
I -satisfied set ;
for psi being wff string of S st [x,psi] in (R3e S) . X holds
b3 -TruthEval b5 = 1let psi be
wff string of
S;
( [x,psi] in (R3e S) . X implies b2 -TruthEval b4 = 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 (R3e S) . X
;
b2 -TruthEval b4 = 1then D1:
(
[x,psi] in S -sequents &
[X,[x,psi]] in P3e S )
by Lm1e;
then
X in dom (P3e 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 Rule3e Seqts
by D1, DefP3e;
then consider r being
relational Element of
S,
T1,
T2 being
abs (ar r) -element Element of
(AllTermsOf S) * such that D2:
(
seqt `1 = {(r -compound T1)} \/ { ((<*(TheEqSymbOf S)*> ^ (TT1 . j)) ^ (TT2 . j)) where j is Element of Seg (abs (ar r)), TT1, TT2 is Function of (Seg (abs (ar r))),(((AllSymbolsOf S) *) \ {{}}) : ( TT1 = T1 & TT2 = T2 ) } &
seqt `2 = r -compound T2 )
by Def3e;
reconsider psi0 =
psi as
0wff string of
S by CC0, D2, FOMODEL0:29;
reconsider phi1 =
r -compound T1 as
0wff string of
S ;
reconsider rr =
(S -firstChar) . psi0 as
relational Element of
S ;
reconsider Fam =
{ ((<*(TheEqSymbOf S)*> ^ (TT1 . j)) ^ (TT2 . j)) where j is Element of Seg (abs (ar r)), TT1, TT2 is Function of (Seg (abs (ar r))),(((AllSymbolsOf S) *) \ {{}}) : ( TT1 = T1 & TT2 = T2 ) } null {phi1} as
Subset of
x by D2, CC0, FOMODEL0:29;
(
((<*r*> ^ ((S -multiCat) . T1)) . 1) \+\ r = {} &
((<*r*> ^ ((S -multiCat) . T2)) . 1) \+\ r = {} )
;
then
(
(<*r*> ^ ((S -multiCat) . T1)) . 1
= r &
(<*r*> ^ ((S -multiCat) . T2)) . 1
= r &
psi0 = <*r*> ^ ((S -multiCat) . T2) )
by D2, CC0, FOMODEL0:29;
then D3:
(
(S -firstChar) . phi1 = r &
rr = r &
psi0 = <*r*> ^ ((S -multiCat) . T2) )
by FOMODEL0:6;
then D4:
(
T1 = SubTerms phi1 &
T2 = SubTerms psi0 )
by FOMODEL1:def 38;
reconsider y =
{phi1} null Fam as
Subset of
x by D2, CC0, FOMODEL0:29;
DD6:
{phi1} = y
;
end; hence
(R3e S) . X is
S -correct
by FOMODEL2:def 44;
verum end;
hence
R3e S is Correct
by RuleCorr; verum