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