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;
0 <= k by NAT_1:2;
hence ex k being Nat st i = k by A1, A2; :: thesis: verum