let n be non prime Element of 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 consider p being Prime such that
A1: p divides n by Lm2;
thus ex p being Prime st
( p divides n & p <> n ) by A1; :: thesis: verum