let p, q be ExtReal; :: thesis: ( q in REAL implies ].p,q.] c= REAL )
assume A1: 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 A2: x in ].p,q.] ; :: thesis: x in REAL
then A3: p < x by Th2;
x <= q by A2, Th2;
hence x in REAL by A1, A3, XXREAL_0:47; :: thesis: verum