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 such that
A3: for n being Nat holds seq . n < r2 by A2;
defpred S₁[ Real] means ex n being Nat st c₁ = seq . n;
consider X being Subset of REAL such that
A4: for p being Element of REAL holds
( p in X iff S₁[p] ) from SUBSET_1:sch 3();

A5: now :: thesis: ex r being Real st
for p being Real st p in X holds
p <= r

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

end;

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

proof

given r being Real such that A7: for p being Real 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 ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not p in X or p <= r )
thus ( not p in X or p <= r ) by A7; :: thesis: verum

end;

take g = upper_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 A8: 0 < s ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not s <= |.((seq . b₂) - g).| )
seq . 0 in X by A4;
then consider p1 being Real such that
A9: p1 in X and
A10: (upper_bound X) - s < p1 by A6, A8, Def1;
consider n1 being Nat such that
A11: p1 = seq . n1 by A4, A9;
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).| )
assume n <= m ; :: thesis: not s <= |.((seq . m) - g).|
then seq . n <= seq . m by A1, SEQM_3:6;
then g + (- s) < seq . m by A10, A11, XXREAL_0:2;
then A12: - s < (seq . m) - g by XREAL_1:20;
seq . m in X by A4;
then seq . m <= g by A6, A5, Def1;
then (seq . m) + 0 < g + s by A8, XREAL_1:8;
then (seq . m) - g < s by XREAL_1:19;
hence not s <= |.((seq . m) - g).| by A12, SEQ_2:1; :: thesis: verum