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