let seq be Real_Sequence; :: thesis: ( seq is non-decreasing & seq is bounded_above implies seq is convergent )
assume that
A1: seq is non-decreasing and
A2: seq is bounded_above ; :: thesis: seq is convergent
consider r2 being real number such that
A3: for n being Element of NAT holds seq . n < r2 by A2, SEQ_2:def 3;
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: now

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

end;

A6: ( ex r being real number st
for p being real number st p in X holds
p <= r implies X is bounded_above )

proof

given r being real number such that G1: for p being real number st p in X holds
p <= r ; :: thesis: X is bounded_above
take r ; :: according to XXREAL_2:def 10 :: thesis: r is UpperBound of X
let p be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( not p in X or p <= r )
thus ( not p in X or p <= r ) by G1; :: thesis: verum

end;

take g = upper_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 A7: 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) )
seq . 0 in X by A4;
then consider p1 being real number such that
A8: p1 in X and
A9: (upper_bound X) - s < p1 by A6, A7, Def4;
consider n1 being Element of NAT such that
A10: p1 = seq . n1 by A4, A8;
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 . n <= seq . m by A1, SEQM_3:12;
then g + (- s) < seq . m by A9, A10, XXREAL_0:2;
then A11: - s < (seq . m) - g by XREAL_1:22;
seq . m in X by A4;
then seq . m <= g by A6, A5, Def4;
then (seq . m) + 0 < g + s by A7, XREAL_1:10;
then (seq . m) - g < s by XREAL_1:21;
hence not s <= abs ((seq . m) - g) by A11, SEQ_2:9; :: thesis: verum