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

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