let p, q be ExtReal; :: thesis: ( p in REAL & q in REAL implies [.p,q.] c= REAL )
assume that
A1: p in REAL and
A2: q in REAL ; :: thesis: [.p,q.] c= REAL
let x be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not x in [.p,q.] or x in REAL )
assume A3: x in [.p,q.] ; :: thesis: x in REAL
then A4: p <= x by Th1;
x <= q by A3, Th1;
hence x in REAL by A1, A2, A4, XXREAL_0:45; :: thesis: verum