theorem Th23: :: XXREAL_2:23

for x, y being ExtReal holds y is UpperBound of [.x,y.[