for A being Interval
for x, y being Real st 0 <= x & y = diameter A holds
x * y = diameter (x ** A)