set E = TheEqSymbOf S;
set phi1 = (<*(TheEqSymbOf S)*> ^ t1) ^ t2;
set phi2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t3;
set phi3 = (<*(TheEqSymbOf S)*> ^ t1) ^ t3;
reconsider seqt = [{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] as Element of S -sequents by Def2;
{} null S is S -sequents-like ;
then reconsider Seqts = {} as empty Subset of (S -sequents) ;
seqt Rule3a {} ;
then [Seqts,seqt] in P#3a S by Def37;
then seqt in (R#3a S) . Seqts by Lm27;
hence for b₁ being object st b₁ = [{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] holds
b₁ is 1, {} ,{(R#3a S)} -derivable by Lm7; :: thesis: verum