let n be Nat; :: 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 ( - n >= 0 & n + (- n) >= 0 + n ) ;
hence n = 0 ; :: thesis: verum
end;
thus ( n = 0 implies - n is Element of NAT ) ; :: thesis: verum