let p, q be ext-real number ; :: 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 Th4;
hence x in REAL by XXREAL_0:48; :: thesis: verum