deffunc H_{1}( Element of X, Element of REAL ) -> Element of [: the carrier of X,REAL:] = [$1,$2];

defpred S_{1}[ Element of X, Real] means f . $1 <= $2;

{ H_{1}(x,y) where x is Element of X, y is Element of REAL : S_{1}[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)) ; :: thesis: verum

defpred S

{ H

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)) ; :: thesis: verum