theorem Th2: :: RCOMP_3:2

for X being non empty real-membered bounded_above set
for Y being closed Subset of REAL st X c= Y holds
upper_bound X in Y