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