set AF = AllFormulasOf S;
reconsider phi11 = phi1 as Element of AllFormulasOf S by FOMODEL2:16;
reconsider Phi2 = Phi \/ {phi11} as finite Subset of (AllFormulasOf S) ;
[Phi2,phi2] is S -sequent-like ;
hence [(Phi \/ {phi1}),phi2] is S -sequent-like ; :: thesis: verum