set FF = AllFormulasOf S;
let x be Element of AllFormulasOf S; :: thesis: x is wff
x in AllFormulasOf S ;
then consider phi being string of S such that
A1: ( x = phi & ex m being Nat st phi is m -wff ) ;
thus x is wff by A1; :: thesis: verum