deffunc H₁( Element of , Element of REAL ) -> Element of [:the carrier of X,REAL :] = [$1,$2];
defpred S₁[ Element of , Element of REAL ] means f . $1 <= R_EAL $2;
{ H₁(x,y) where x is Element of , y is Element of REAL : S₁[x,y] } is Subset of from DOMAIN_1:sch 9();
hence { [x,y] where x is Element of , y is Element of REAL : f . x <= R_EAL y } is Subset of ; :: thesis: verum