theorem Th5: :: PYTHTRIP:5

for m, n being Nat st m ^2 = n ^2 holds
m = n