set Q = S -sequents ;
set psi = (l,t) SubstIn phi;
reconsider Sq = [{((l,t) SubstIn phi)},(<*l*> ^ phi)] as S -sequent-like object ;
reconsider SQ = {} null S as S -sequents-like set ;
reconsider seqt = Sq as Element of S -sequents by Def2;
reconsider Seqts = SQ as Element of bool (S -sequents) by Def3;
seqt Rule4 Seqts ;
then [Seqts,seqt] in P#4 S by Def41;
then Sq in (R#4 S) . SQ by Th3;
hence for b₁ being object st b₁ = [{((l,t) SubstIn phi)},(<*l*> ^ phi)] holds
b₁ is 1, {} ,{(R#4 S)} -derivable by Lm7; :: thesis: verum