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