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