theorem Th6: :: XXREAL_1:6

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