theorem Th16: :: INTEGRA2:16

for r being Real
for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds
upper_bound (r ** X) = r * (lower_bound X)