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

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