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