let x be set ; for p, q being ExtReal holds
( not x in ].p,q.] or x in ].p,q.[ or x = q )
let p, q be ExtReal; ( not x in ].p,q.] or x in ].p,q.[ or x = q )
assume A1:
x in ].p,q.]
; ( x in ].p,q.[ or x = q )
then reconsider s = x as ExtReal ;
A2:
p < s
by A1, Th2;
s <= q
by A1, Th2;
then
( q = s or s < q )
by XXREAL_0:1;
hence
( x in ].p,q.[ or x = q )
by A2, Th4; verum