let i be Integer; :: thesis: ( i < 0 implies ex k being Nat st i = - k )
assume A1: i < 0 ; :: thesis: ex k being Nat st i = - k
i in INT by INT_1:def 2;
then consider k being Nat such that
A2: ( i = k or i = - k ) by INT_1:def 1;
thus ex k being Nat st i = - k by A1, A2, NAT_1:2; :: thesis: verum