theorem :: MOEBIUS3:49

for n being non zero Nat holds support (ppf n) c= Seg n