theorem :: XXREAL_2:59

for X, Y being ext-real-membered set st X c= Y holds
sup X <= sup Y