theorem :: MOEBIUS3:69

for n being Nat holds (Partial_Sums Basel-seq) . n >= 0