for i, j being Element of NAT st x. i = x. j holds
i = j ;