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

hence ex p being Prime st p divides n by INT_2:28, NAT_D:6; :: thesis: verum

end;

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

then ex p being Element of NAT st
( p is prime & p divides n ) by A1, Th1, INT_2:31;
hence ex p being Prime st p divides n ; :: thesis: verum

end;

end;