for n being Nat
for x being object st n = {x} holds
x = 0