for m, n being Element of NAT st prop n = prop m holds
n = m