set R = { [r,s] where r, s is Real : r <= s } ;
{ [r,s] where r, s is Real : r <= s } c= [:REAL,REAL:]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [r,s] where r, s is Real : r <= s } or x in [:REAL,REAL:] )
assume x in { [r,s] where r, s is Real : r <= s } ; :: thesis: x in [:REAL,REAL:]
then consider r, s being Real such that
A1: ( x = [r,s] & r <= s ) ;
( r in REAL & s in REAL ) by XREAL_0:def 1;
hence x in [:REAL,REAL:] by A1, ZFMISC_1:87; :: thesis: verum

end;

hence { [r,s] where r, s is Real : r <= s } is Relation of REAL ; :: thesis: verum