set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
defpred S₁[ string of S] means ( $1 is wff & $1 is exal );
defpred S₂[ set ] means verum;
deffunc H₁( set ) -> set = $1;
A1: for w being string of S st S₁[w] holds
S₂[w] ;
set IT = { H₁(w) where w is string of S : S₁[w] } ;
{ H₁(w) where w is string of S : S₁[w] } c= { H₁(w) where w is string of S : S₂[w] } from FRAENKEL:sch 1(A1);
hence { phi where phi is string of S : ( phi is wff & phi is exal ) } is Subset of (((AllSymbolsOf S) *) \ {{}}) by DOMAIN_1:18; :: thesis: verum