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