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;