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