theorem Th7: :: XXREAL_1:7

for x being set
for p, q being ExtReal holds
( not x in [.p,q.] or x in [.p,q.[ or x = q )