for X being non empty real-membered set
for Y being real-membered set st X c= Y & Y is bounded_above holds
upper_bound X <= upper_bound Y