theorem Th17: :: MOEBIUS1:17
for m, n being non zero Nat st ( for p being Prime holds p |-count m <= p |-count n ) holds
support (ppf m) c= support (ppf n)