theorem Th1: :: RCOMP_3:1

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