deffunc H1( Element of X, Element of REAL ) -> Element of [: the carrier of X,REAL:] = [$1,$2];
defpred S1[ Element of X, Real] means f . $1 <= $2;
{ H1(x,y) where x is Element of X, y is Element of REAL : S1[x,y] } is Subset of [: the carrier of X,REAL:]
from DOMAIN_1:sch 9();
hence
{ [x,y] where x is Element of X, y is Element of REAL : f . x <= y } is Subset of (Prod_of_RLS (X,RLS_Real))
; verum