:: deftheorem Def7 defines the_only_divisor_of NUMBER08:def 7 :
for n being Nat st n is having_exactly_one_prime_divisor holds
for b₂ being Prime holds
( b₂ = the_only_divisor_of n iff ( b₂ divides n & ( for r being Prime st r <> b₂ holds
not r divides n ) ) );