theorem Impor2: :: MOEBIUS3:31

for n being non trivial Nat holds Sum (Basel-seq,n,1) < Sum (Reci-seq1,n,1)