theorem NEW: :: COMPLEX3:64

for a, b, c, n being positive Real
for m being non negative Real st (a to_power m) + (b to_power m) <= c to_power m holds
(a to_power (m + n)) + (b to_power (m + n)) < c to_power (m + n)