set SS = AllSymbolsOf S;
set AF = AtomicFormulasOf S;
defpred S₁[ Element of ((AllSymbolsOf S) *) \ {{}}] means $1 is 0wff ;
{ phi where phi is Element of ((AllSymbolsOf S) *) \ {{}} : S₁[phi] } is Subset of (((AllSymbolsOf S) *) \ {{}}) from DOMAIN_1:sch 7();
hence AtomicFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}}) ; :: thesis: verum