set FF = AllFormulasOf S;
(H1 null H1) \/ (H2 null H2) c= AllFormulasOf S ;
hence for b₁ being set st b₁ = H1 \/ H2 holds
b₁ is S -premises-like by DefPremLike; :: thesis: verum