set SS = AllSymbolsOf S;

set strings = ((AllSymbolsOf S) *) \ {{}};

defpred S_{1}[ string of S] means ( $1 is wff & $1 is exal );

defpred S_{2}[ set ] means verum;

deffunc H_{1}( set ) -> set = $1;

A1: for w being string of S st S_{1}[w] holds

S_{2}[w]
;

set IT = { H_{1}(w) where w is string of S : S_{1}[w] } ;

{ H_{1}(w) where w is string of S : S_{1}[w] } c= { H_{1}(w) where w is string of S : S_{2}[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

set strings = ((AllSymbolsOf S) *) \ {{}};

defpred S

defpred S

deffunc H

A1: for w being string of S st S

S

set IT = { H

{ H

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