theorem Th31: :: BASEL_2:31

for m being Nat holds Sum (Basel-seq,m) <= Basel-seq2 . m