let seq be Real_Sequence; :: thesis: ( seq is V48() & seq is bounded_below implies seq is convergent )
assume that
A1: seq is V48() and
A2: seq is bounded_below ; :: thesis: seq is convergent
defpred S1[ Real] means ex n being Nat st c1 = seq . n;
consider X being Subset of REAL such that
A3: for p being Element of REAL holds
( p in X iff S1[p] ) from SUBSET_1:sch 3();
 take g = lower_bound X; :: according to SEQ_2:def 6 :: thesis: for b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= |.((seq . b3) - g).| ) )
let s be Real; :: thesis: ( s <= 0 or ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not s <= |.((seq . b2) - g).| ) )
assume A4: 0 < s ; :: thesis: ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not s <= |.((seq . b2) - g).| )
A5: ( ex r being Real st
for p being Real st p in X holds
r <= p implies X is bounded_below )
proof
given r being Real such that A6: for p being Real st p in X holds
r <= p ; :: thesis: X is bounded_below
take r ; :: according to XXREAL_2:def 9 :: thesis: r is LowerBound of X
let p be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not p in X or r <= p )
thus ( not p in X or r <= p ) by A6; :: thesis: verum
end;
seq . 0 in X by A3;
then consider p1 being Real such that
A7: p1 in X and
A8: p1 < (lower_bound X) + s by A5, A4, Def2;
consider n1 being Nat such that
A9: p1 = seq . n1 by A3, A7;
take n = n1; :: thesis: for b1 being set holds
( not n <= b1 or not s <= |.((seq . b1) - g).| )
let m be Nat; :: thesis: ( not n <= m or not s <= |.((seq . m) - g).| )
consider r1 being Real such that
A10: for n being Nat holds r1 < seq . n by A2;
A11: now :: thesis: ex r being Real st
for p being Real st p in X holds
r <= p
take r = r1; :: thesis: for p being Real st p in X holds
r <= p
let p be Real; :: thesis: ( p in X implies r <= p )
assume p in X ; :: thesis: r <= p
then ex n1 being Nat st p = seq . n1 by A3;
hence r <= p by A10; :: thesis: verum
end;
seq . m in X by A3;
then 0 + g <= seq . m by A5, A11, Def2;
then A12: 0 <= (seq . m) - g by XREAL_1:19;
assume n <= m ; :: thesis: not s <= |.((seq . m) - g).|
then seq . m <= seq . n by A1, SEQM_3:8;
then seq . m < g + s by A8, A9, XXREAL_0:2;
then A13: (seq . m) - g < s by XREAL_1:19;
- s < - 0 by A4;
hence not s <= |.((seq . m) - g).| by A13, A12, SEQ_2:1; :: thesis: verum