for X being non empty Subset of ExtREAL
for Y being non empty Subset of REAL st X = Y & X is bounded_above holds
( Y is bounded_above & sup X = upper_bound Y ) by Th1;