theorem :: COMPLEX3:43

for a, b, c, d being positive Real
for n being Real st a + b = c + d & (a to_power n) + (b to_power n) <> (c to_power n) + (d to_power n) holds
a * b <> c * d by ABCD;