defpred S₁[ set ] means $1 in X;
deffunc H₁( Real) -> Element of REAL = - $1;
thus { H₁(r3) where r3 is Real : S₁[r3] } is Subset of REAL from DOMAIN_1:sch 8(); :: thesis: verum