let seq be Real_Sequence; :: thesis: ( seq is non-increasing & seq is bounded_below implies seq is convergent )
assume that
A1: seq is non-increasing and
A2: seq is bounded_below ; :: thesis: seq is convergent
defpred S₁[ Real] means ex n being Element of NAT st c₁ = seq . n;
consider X being Subset of REAL such that
A3: for p being Real holds
( p in X iff S₁[p] ) from SUBSET_1:sch 3();
take g = lower_bound X; :: according to SEQ_2:def 6 :: thesis: for b₁ being set holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= abs ((seq . b₃) - g) ) )
let s be real number ; :: thesis: ( s <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not s <= abs ((seq . b₂) - g) ) )
assume A4: 0 < s ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not s <= abs ((seq . b₂) - g) )
A5: ( ex r being real number st
for p being real number st p in X holds
r <= p implies X is bounded_below )

proof

given r being real number such that G1: for p being real number 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 ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not p in X or r <= p )
thus ( not p in X or r <= p ) by G1; :: thesis: verum

end;

seq . 0 in X by A3;
then consider p1 being real number such that
A6: p1 in X and
A7: p1 < (lower_bound X) + s by A5, A4, Def5;
consider n1 being Element of NAT such that
A8: p1 = seq . n1 by A3, A6;
take n = n1; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not s <= abs ((seq . b₁) - g) )
let m be Element of NAT ; :: thesis: ( not n <= m or not s <= abs ((seq . m) - g) )
consider r1 being real number such that
A9: for n being Element of NAT holds r1 < seq . n by A2, SEQ_2:def 4;

A10: now

take r = r1; :: thesis: for p being real number st p in X holds
r <= p
let p be real number ; :: thesis: ( p in X implies r <= p )
assume p in X ; :: thesis: r <= p
then ex n1 being Element of NAT st p = seq . n1 by A3;
hence r <= p by A9; :: thesis: verum

end;

seq . m in X by A3;
then 0 + g <= seq . m by A5, A10, Def5;
then A11: 0 <= (seq . m) - g by XREAL_1:21;
assume n <= m ; :: thesis: not s <= abs ((seq . m) - g)
then seq . m <= seq . n by A1, SEQM_3:14;
then seq . m < g + s by A7, A8, XXREAL_0:2;
then A12: (seq . m) - g < s by XREAL_1:21;
- s < - 0 by A4, XREAL_1:26;
hence not s <= abs ((seq . m) - g) by A12, A11, SEQ_2:9; :: thesis: verum