for A being non empty Interval
for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).] holds
( B = ].(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )