set AF = AtomicFormulasOf S;
let phi be Element of AtomicFormulasOf S; :: thesis: phi is 0wff
phi in AtomicFormulasOf S ;
then consider x being string of S such that
A1: ( phi = x & x is 0wff ) ;
thus phi is 0wff by A1; :: thesis: verum