assume A3:
lim_sup seq <= r
; :: thesis: for s being Real st 0< s holds ex n being Nat st for k being Nat holds seq .(n + k)< r + s
for s being Real st 0< s holds ex n being Nat st for k being Nat holds seq .(n + k)< r + s
let s be Real; :: thesis: ( 0< s implies ex n being Nat st for k being Nat holds seq .(n + k)< r + s ) assume A4:
0< s
; :: thesis: ex n being Nat st for k being Nat holds seq .(n + k)< r + s
ex n being Nat st for k being Nat holds seq .(n + k)< r + s