theorem Th22: :: XXREAL_2:22

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