theorem Th71: :: XXREAL_2:71

for x, y being ExtReal
for A being ext-real-membered set st x <= y & x is UpperBound of A holds
y is UpperBound of A