:: deftheorem defines PrimeDivisors NUMBER12:def 3 :
for n being Integer holds PrimeDivisors n = { k where k is Prime : k divides n } ;