theorem :: MOEBIUS3:50

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