theorem Th33: :: XXREAL_2:33
for x, y being ExtReal st x <= y holds
( [.x,y.] is left_end & [.x,y.] is right_end )