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