theorem :: NEWTON06:45
for a, b, c, d being positive Real st a * b = c * d & a * c = b * d holds
a = d