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 Lm10;
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 Def2;
then [Seqts,seqt] in P2 S by DefP2;
then seqt in (R2 S) . Seqts by Lm1;
then {seqt} c= (R2 S) . Seqts by ZFMISC_1:31;
then {seqt} is {} ,{(R2 S)} -derivable by Lm9;
hence for b₁ being set st b₁ = {[{},((<*(TheEqSymbOf S)*> ^ t) ^ t)]} holds
b₁ is {(R2 S)} -derivable ; :: thesis: verum