theorem Th34: :: XXREAL_2:34

for x, y being ExtReal st x < y holds
[.x,y.[ is left_end