theorem :: URYSOHN2:33

for A being non empty Subset of REAL
for x being Real st x > 0 & x ** A is bounded_below holds
A is bounded_below by Lm2;