theorem Th27: :: XXREAL_1:27

for p, q being ExtReal st p <= q holds
[.q,p.[ = {}