set E = TheEqSymbOf S;
set SS = AllSymbolsOf S;
set T = S -termsOfMaxDepth ;
set C = S -multiCat ;
reconsider phi = (<*(TheEqSymbOf S)*> ^ t) ^ t as wff string of S by Lm2;
reconsider Seqts = {} as Element of bool (S -sequents) by XBOOLE_1:2;
reconsider seqt = [{},phi] as Element of S -sequents ;
( seqt `1 is empty & seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t ) by MCART_1:7;
then seqt Rule2 {} by Def20;
then [Seqts,seqt] in P#2 S by Def33;
then seqt in (R#2 S) . Seqts by Lm26;
then {seqt} c= (R#2 S) . Seqts by ZFMISC_1:31;
then {seqt} is {} ,{(R#2 S)} -derivable by Lm19;
hence for b₁ being set st b₁ = {[{},((<*(TheEqSymbOf S)*> ^ t) ^ t)]} holds
b₁ is {(R#2 S)} -derivable ; :: thesis: verum