let n be natural number ; :: thesis: ( n <> 1 implies ex p being Prime st p divides n )
assume A1: n <> 1 ; :: thesis: ex p being Prime st p divides n

per cases ( n is empty or not n is empty ) ;

suppose n is empty ; :: thesis: ex p being Prime st p divides n

then 2 divides n by NAT_D:6;
hence ex p being Prime st p divides n by INT_2:44; :: thesis: verum

end;

suppose not n is empty ; :: thesis: ex p being Prime st p divides n

then n >= 2 by A1, Th1;
then consider p being Element of NAT such that
A2: ( p is prime & p divides n ) by INT_2:48;
thus ex p being Prime st p divides n by A2; :: thesis: verum

end;

end;