theorem Multiply1: :: NUMBER12:58

for x, y, z being positive Real holds ((x / y) * (y / z)) * (z / x) = 1