let n be non prime Nat; :: thesis: ( n <> 1 implies ex p being Prime st
( p divides n & p <> n ) )
assume n <> 1 ; :: thesis: ex p being Prime st
( p divides n & p <> n )
then ex p being Prime st p divides n by Lm2;
hence ex p being Prime st
( p divides n & p <> n ) ; :: thesis: verum