set FF = AllFormulasOf S;
phi in AllFormulasOf S by FOMODEL2:16;
then ( {phi} c= AllFormulasOf S & {phi} is finite ) by ZFMISC_1:31;
hence for b₁ being set st b₁ = {phi} holds
b₁ is S -premises-like by Def64; :: thesis: verum