set AF = AtomicFormulasOf S;
set phi = the 0wff string of S;
the 0wff string of S in AtomicFormulasOf S ;
hence for b₁ being set st b₁ = AtomicFormulasOf S holds
not b₁ is empty ; :: thesis: verum