theorem Th14: :: INTEGRA2:14

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