theorem :: INTEGRA2:12

for r being Real
for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds
r ** X is bounded_above