theorem Th2: :: FIELD_3:1

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