].-infty,r.[ c= REAL
proof
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;
hence ].-infty,r.[ is Subset of REAL ; :: thesis: verum