theorem Th21: :: XXREAL_2:21

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