theorem Th28: :: IRRAT_1:28

for n being Nat st n >= 1 holds
dseq . n <= Sum eseq