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
consider r1 being real number such that
A3: for n being Element of NAT holds r1 < seq . n by A2, SEQ_2:def 4;
defpred S₁[ Real] means ex n being Element of NAT st c₁ = seq . n;
consider X being Subset of REAL such that
A4: for p being Real holds
( p in X iff S₁[p] ) from SUBSET_1:sch 3();
A5: seq . 0 in X by A4;
A6: ( X is bounded_below iff ex r being real number st
for p being real number st p in X holds
r <= p ) by Def2;

A7: 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 A4;
hence r <= p by A3; :: thesis: verum

end;

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 A8: 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) )
then consider p1 being real number such that
A9: p1 in X and
A10: p1 < (lower_bound X) + s by A5, A6, Def5;
consider n1 being Element of NAT such that
A11: p1 = seq . n1 by A4, A9;
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) )
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 A10, A11, XXREAL_0:2;
then A12: (seq . m) - g < s by XREAL_1:21;
seq . m in X by A4;
then 0 + g <= seq . m by A6, A7, Def5;
then A13: 0 <= (seq . m) - g by XREAL_1:21;
- s < - 0 by A8, XREAL_1:26;
hence abs ((seq . m) - g) < s by A12, A13, SEQ_2:9; :: thesis: verum