theorem :: ZF_LANG1:77

for x being Variable ex i being Element of NAT st x = x. i