let p, q be ExtReal; :: 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 A1: x in ].p,q.[ ; :: thesis: x in REAL
then A2: p < x by Th4;
x < q by A1, Th4;
hence x in REAL by A2, XXREAL_0:48; :: thesis: verum