].-infty,r.[ c= REAL

proof

hence
].-infty,r.[ is Subset of REAL
; :: thesis: verum
let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in ].-infty,r.[ or x in REAL )

assume x in ].-infty,r.[ ; :: thesis: x in REAL

then ( -infty < x & x < r ) by XXREAL_1:4;

hence x in REAL by XXREAL_0:48; :: thesis: verum

end;assume x in ].-infty,r.[ ; :: thesis: x in REAL

then ( -infty < x & x < r ) by XXREAL_1:4;

hence x in REAL by XXREAL_0:48; :: thesis: verum