consider p being Element of NAT such that
A1: ( p is prime & p divides n ) by NAT_2:29, INT_2:31;
reconsider p = p as natural number ;
take p ; :: thesis: ( p is Divisor of n & p is prime )
thus ( p is Divisor of n & p is prime ) by A1, Def2; :: thesis: verum