theorem :: XXREAL_2:63

for X, Y being ext-real-membered set st ( for x being ExtReal st x in X holds
ex y being ExtReal st
( y in Y & x <= y ) ) holds
sup X <= sup Y