theorem :: NUMBER08:75

for p being Prime holds the_only_divisor_of p = p by Def7;