for seq being Real_Sequence st seq is summable & ( for n being Nat holds seq . n > 0 ) holds
Sum seq > 0