let n be Nat; :: thesis: ( n is zero implies not n is having_exactly_one_prime_divisor )
assume A1: n is zero ; :: thesis: not n is having_exactly_one_prime_divisor
given p being Prime such that p divides n and
A2: for r being Prime st r <> p holds
not r divides n ; :: according to NUMBER08:def 6 :: thesis: contradiction
ex p1 being Prime st p < p1 by NEWTON:72;
hence contradiction by A1, A2, INT_2:12; :: thesis: verum