for n being Nat st n <> 1 holds
ex p being Prime st p divides n