theorem Th8: :: XXREAL_1:8

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