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 Def2;
reconsider Seqts = SQ as Element of bool (S -sequents) by Def3;
( (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 Def25;
then [Seqts,seqt] in P#4 S by Def38;
then Sq in (R#4 S) . SQ by Th2;
hence for b₁ being set st b₁ = [{((l,t) SubstIn phi)},(<*l*> ^ phi)] holds
b₁ is 1, {} ,{(R#4 S)} -derivable by Lm50; :: thesis: verum