theorem :: MOEBIUS1:63

for n being non zero Nat
for p being Prime holds { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } c= Seg n