theorem :: ZF_LANG1:76

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