let n be Nat; :: 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 zero or not n is zero ) ;
suppose n is zero ; :: 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 zero ; :: 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;