set EF = ExFormulasOf S;
let x be Element of ExFormulasOf S; :: thesis: ( x is exal & x is wff )
x in ExFormulasOf S ;
then consider w being string of S such that
A1: ( x = w & w is wff & w is exal ) ;
reconsider phi = x as wff exal string of S by A1;
phi is wff exal string of S ;
hence ( x is exal & x is wff ) ; :: thesis: verum