theorem Th5: :: PYTHTRIP:5

for m, n being Element of NAT st m ^2 = n ^2 holds
m = n