theorem Th24: :: XXREAL_2:24

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