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 ;
reconsider Seqts = {} as Element of bool (S -sequents) by XBOOLE_1:2;
reconsider seqt = [{},phi] as Element of S -sequents ;
seqt Rule2 {} ;
then [Seqts,seqt] in P#2 S by Def36;
then seqt in (R#2 S) . Seqts by Lm27;
then {seqt} is {} ,{(R#2 S)} -derivable by Lm20, ZFMISC_1:31;
hence for b₁ being set st b₁ = {[{},((<*(TheEqSymbOf S)*> ^ t) ^ t)]} holds
b₁ is {(R#2 S)} -derivable ; :: thesis: verum