for i being Nat
for x being object st x in i holds
x is Element of NAT