theorem Th5: :: XXREAL_1:5

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