set Q = S -sequents ;
set psi = (l,t) SubstIn phi;
reconsider Sq = [{((l,t) SubstIn phi)},(<*l*> ^ phi)] as S -sequent-like set ;
reconsider SQ = {} null S as S -sequents-like set ;
reconsider seqt = Sq as Element of S -sequents by DefSeqtLike;
reconsider Seqts = SQ as Element of bool (S -sequents) by DefSeqtLike2;
( (seqt `1) \+\ {((l,t) SubstIn phi)} = {} & (seqt `2) \+\ (<*l*> ^ phi) = {} ) ;
then ( Seqts = {} & seqt `1 = {((l,t) SubstIn phi)} & seqt `2 = <*l*> ^ phi ) by FOMODEL0:29;
then seqt Rule4 Seqts by Def4;
then [Seqts,seqt] in P4 S by DefP4;
then Sq in (R4 S) . SQ by Th3;
hence for b₁ being set st b₁ = [{((l,t) SubstIn phi)},(<*l*> ^ phi)] holds
b₁ is 1, {} ,{(R4 S)} -derivable by Lm22; :: thesis: verum