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 )

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

proof

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

then ( - n >= 0 & n + (- n) >= 0 + n ) ;

hence n = 0 ; :: thesis: verum

end;then ( - n >= 0 & n + (- n) >= 0 + n ) ;

hence n = 0 ; :: thesis: verum