let q, p be ext-real number ; :: thesis: ( q in REAL implies ].p,q.] c= REAL )
assume Z: q 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 Th2;
hence x in REAL by Z, XXREAL_0:47; :: thesis: verum