for n being non prime Element of NAT st n <> 1 holds
ex p being Prime st
( p divides n & p <> n )