let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n > 0 ) & ex m being Nat st
for n being Nat st n >= m holds
(s . (n + 1)) / (s . n) >= 1 implies not s is summable )
assume that
A1: for n being Nat holds s . n > 0 and
A2: ex m being Nat st
for n being Nat st n >= m holds
(s . (n + 1)) / (s . n) >= 1 ; :: thesis: not s is summable
consider m being Nat such that
A3: for n being Nat st n >= m holds
(s . (n + 1)) / (s . n) >= 1 by A2;
defpred S₁[ Nat] means s . (m + $1) >= s . m;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: s . (m + k) >= s . m ; :: thesis: S₁[k + 1]
( s . (m + k) > 0 & (s . ((m + k) + 1)) / (s . (m + k)) >= 1 ) by A1, A3, NAT_1:11;
then s . ((m + k) + 1) >= s . (m + k) by XREAL_1:191;
hence S₁[k + 1] by A5, XXREAL_0:2; :: thesis: verum

end;

A6: S₁[ 0 ] ;
A7: for k being Nat holds S₁[k] from NAT_1:sch 2(A6, A4);
A8: for k being Nat ex n being Nat st
( n >= k & not |.((s . n) - 0).| < s . m )

proof

let k be Nat; :: thesis: ex n being Nat st
( n >= k & not |.((s . n) - 0).| < s . m )
take n = m + k; :: thesis: ( n >= k & not |.((s . n) - 0).| < s . m )
s . n >= s . m by A7;
hence ( n >= k & not |.((s . n) - 0).| < s . m ) by NAT_1:11, SEQ_2:1; :: thesis: verum

end;

s . m > 0 by A1;
then ( not lim s = 0 or not s is convergent ) by A8, SEQ_2:def 7;
hence not s is summable by Th4; :: thesis: verum