theorem :: NUMBER18:38

for a, b being Nat st a divides b holds
PrimeDivisors a c= PrimeDivisors b