let S be Language; :: thesis: for phi being wff string of S holds phi in AllFormulasOf S
let phi be wff string of S; :: thesis: phi in AllFormulasOf S
set AF = AllFormulasOf S;
consider m being Nat such that
B0: phi is m -wff by DefWff2;
thus phi in AllFormulasOf S by B0; :: thesis: verum