let p be Integer; :: thesis: ( p is prime implies p is natural )
assume p is prime ; :: thesis: p is natural
then p > 1 by INT_2:def 4;
then p >= 0 ;
then p in NAT by INT_1:3;
hence p is natural ; :: thesis: verum