let p, q be ext-real number ; :: thesis: ( p in REAL implies [.p,q.[ c= REAL )
assume Z: p in REAL ; :: thesis: [.p,q.[ c= REAL
let x be ext-real number ; :: according to MEMBERED:def 8 :: thesis: ( not x in [.p,q.[ or x in REAL )
assume x in [.p,q.[ ; :: thesis: x in REAL
then ( p <= x & x < q ) by Th3;
hence x in REAL by Z, XXREAL_0:46; :: thesis: verum