let n be Nat; :: thesis: ( n <> 1 implies ex p being Prime st p divides n )
assume A2: n <> 1 ; :: thesis: ex p being Prime st p divides n

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

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

hence ex p being Prime st p divides n ; :: thesis: verum

end;

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

then ex p being Prime st
( p divides n & p <> n ) by A2, Th4;
hence ex p being Prime st p divides n ; :: thesis: verum

end;

end;