set FF = AllFormulasOf S;
reconsider HH = H as finite Subset of (AllFormulasOf S) by Def4;
[HH,phi] is S -sequent-like ;
hence [H,phi] is S -sequent-like ; :: thesis: verum