theorem Th31: :: XXREAL_2:31

for x, y being ExtReal st x < y holds
sup [.x,y.[ = y