let n be Nat; :: thesis: ( n <> 1 implies ex p being Prime st p divides n )
A1: n in NAT by ORDINAL1:def 12;
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 A1, A2, Th4;
hence ex p being Prime st p divides n ; :: thesis: verum
end;
end;