let a be Real; :: thesis: for s1 being Real_Sequence st s1 is convergent & ( for n being Nat holds s1 . n >= a ) holds

lim s1 >= a

let s1 be Real_Sequence; :: thesis: ( s1 is convergent & ( for n being Nat holds s1 . n >= a ) implies lim s1 >= a )

assume that

A1: s1 is convergent and

A2: for n being Nat holds s1 . n >= a ; :: thesis: lim s1 >= a

set s = seq_const a;

.= a by SEQ_1:57 ;

hence lim s1 >= a by A1, A3, SEQ_2:18; :: thesis: verum

lim s1 >= a

let s1 be Real_Sequence; :: thesis: ( s1 is convergent & ( for n being Nat holds s1 . n >= a ) implies lim s1 >= a )

assume that

A1: s1 is convergent and

A2: for n being Nat holds s1 . n >= a ; :: thesis: lim s1 >= a

set s = seq_const a;

A3: now :: thesis: for n being Nat holds s1 . n >= (seq_const a) . n

lim (seq_const a) =
(seq_const a) . 0
by SEQ_4:26
let n be Nat; :: thesis: s1 . n >= (seq_const a) . n

s1 . n >= a by A2;

hence s1 . n >= (seq_const a) . n by SEQ_1:57; :: thesis: verum

end;s1 . n >= a by A2;

hence s1 . n >= (seq_const a) . n by SEQ_1:57; :: thesis: verum

.= a by SEQ_1:57 ;

hence lim s1 >= a by A1, A3, SEQ_2:18; :: thesis: verum