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 Nat st c₁ = seq . n;
consider X being Subset of REAL such that
A3: for p being Element of 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 object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= |.((seq . b₃) - g).| ) )
let s be Real; :: thesis: ( s <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not s <= |.((seq . b₂) - g).| ) )
assume A4: 0 < s ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not s <= |.((seq . b₂) - 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 b₁ being set holds
( not n <= b₁ or not s <= |.((seq . b₁) - 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