theorem Th11: :: LIOUVIL1:9

for s1, s2 being Real_Sequence st ( for n being Nat holds
( 0 <= s1 . n & s1 . n <= s2 . n ) ) & ex n being Nat st
( 1 <= n & s1 . n < s2 . n ) & s2 is summable holds
( s1 is summable & Sum s1 < Sum s2 )