for X being non empty Subset of ExtREAL
for Y being non empty Subset of REAL st X = Y & Y is bounded_below holds
( X is bounded_below & inf X = lower_bound Y )