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 set ; :: 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 ex r, s being Real st
( x = [r,s] & r <= s ) ;
hence x in [:REAL,REAL:] by ZFMISC_1:106; :: thesis: verum

end;

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