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

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