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