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 ;
TARSKI:def 3 ( 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 }
;
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;
verum
end;
hence
{ [r,s] where r, s is Real : r <= s } is Relation of REAL
; verum