reconsider phi11 = (l1,l2) -SymbolSubstIn phi1 as wff string of S ;
set H1 = H \/ {phi11};
set Sq1 = [(H \/ {phi11}),phi2];
set H2 = H \/ {(<*l1*> ^ phi1)};
set Sq2 = [(H \/ {(<*l1*> ^ phi1)}),phi2];
set R = R5 S;
set Q = S -sequents ;
set x = H;
set SS = AllSymbolsOf S;
set SQ = {[(H \/ {phi11}),phi2]};
set s = l1 SubstWith l2;
reconsider p = phi1 as AllSymbolsOf S -valued FinSequence ;
reconsider seqt = [(H \/ {(<*l1*> ^ phi1)}),phi2] as Element of S -sequents by DefSeqtLike;
reconsider Seqts = {[(H \/ {phi11}),phi2]} as Element of bool (S -sequents) by DefSeqtLike2;
( (seqt `1) \+\ (H \/ {(<*l1*> ^ phi1)}) = {} & (seqt `2) \+\ phi2 = {} ) ;
then B1: ( seqt `1 = H \/ {(<*l1*> ^ phi1)} & seqt `2 = phi2 ) by FOMODEL0:29;
H \/ {((l1 SubstWith l2) . p)} = H \/ {phi11} by FOMODEL0:def 23;
then [(H \/ {((l1 SubstWith l2) . p)}),(seqt `2)] in Seqts by B1, TARSKI:def 1;
then seqt Rule5 Seqts by B1, Def5;
then [Seqts,seqt] in P5 S by DefP5;
then seqt in (R5 S) . Seqts by Th3;
hence for b₁ being set st b₁ = [((H \/ {(<*l1*> ^ phi1)}) null l2),phi2] holds
b₁ is 1,{[(H \/ {((l1,l2) -SymbolSubstIn phi1)}),phi2]},{(R5 S)} -derivable by Lm22; :: thesis: verum