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
A1: phi is m -wff by Def24;
thus phi in AllFormulasOf S by A1; :: thesis: verum