theorem Th9: :: XXREAL_1:9

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