theorem Th6: :: INT_2:6

for n being Nat holds
( - n is Element of NAT iff n = 0 )