let n be natural number ; :: thesis: ( - n is Element of NAT iff n = 0 )
thus ( - n is Element of NAT implies n = 0 ) :: thesis: ( n = 0 implies - n is Element of NAT )

proof

assume - n is Element of NAT ; :: thesis: n = 0
then A1: ( - n >= 0 & n >= 0 ) by NAT_1:2;
then n + (- n) >= 0 + n ;
hence n = 0 by A1, XXREAL_0:1; :: thesis: verum

end;

thus ( n = 0 implies - n is Element of NAT ) ; :: thesis: verum
thus verum ; :: thesis: verum