theorem Th18: :: URYSOHN2:18
for A being non empty Subset of REAL
for x being Real
for y being R_eal st x = y & 0 <= y holds
sup (x ** A) = y * (sup A)