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} ) by ENUMSET1:1;
hence for b₁ being set st b₁ = [{phi1,phi2},phi3] holds
b₁ is S -sequent-like ; :: thesis: verum