let n be Nat; :: thesis: ( n is prime implies n is having_exactly_one_prime_divisor )
assume n is prime ; :: thesis: n is having_exactly_one_prime_divisor
then reconsider n = n as Prime ;
take n ; :: according to NUMBER08:def 6 :: thesis: ( n divides n & ( for r being Prime st r <> n holds
not r divides n ) )
thus ( n divides n & ( for r being Prime st r <> n holds
not r divides n ) ) by Th7; :: thesis: verum