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