let i be Integer; :: thesis: ( not i is negative implies i is natural )
assume not i is negative ; :: thesis: i is natural
then i in NAT by INT_1:3;
hence i is natural ; :: thesis: verum