theorem Th30: :: XXREAL_2:30

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