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