set FF = AllFormulasOf S;
(H1 null H1) \/ (H2 null H2) c= AllFormulasOf S ;
hence H1 \/ H2 is S -premises-like ; :: thesis: verum