reconsider a = upper_bound A as Element of REAL by XREAL_0:def 1;
reconsider p = (Seg 1) --> a as Function of (Seg 1),REAL by FUNCOP_1:45;
A1: dom p = Seg 1 by FUNCOP_1:13;
rng p c= REAL ;
then reconsider p = p as FinSequence of REAL by FINSEQ_1:def 4;
A2: 1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
for n, m being Nat st n in dom p & m in dom p & n < m holds
p . n < p . m
proof
let n, m be Nat; :: thesis: ( n in dom p & m in dom p & n < m implies p . n < p . m )
assume that
A3: n in dom p and
A4: m in dom p ; :: thesis: ( not n < m or p . n < p . m )
n = 1 by A1, A3, FINSEQ_1:2, TARSKI:def 1;
hence ( not n < m or p . n < p . m ) by A1, A4, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum
end;
then A5: p is non empty increasing FinSequence of REAL by SEQM_3:def 1;
upper_bound A in A by RCOMP_1:14;
then for n being Nat st n in Seg 1 holds
p . n in A by FUNCOP_1:7;
then p is FinSequence of A by A1, FINSEQ_2:12;
then A6: rng p c= A by FINSEQ_1:def 4;
len p = 1 by A1, FINSEQ_1:def 3;
then p . (len p) = upper_bound A by A2, FUNCOP_1:7;
hence ex b1 being non empty increasing FinSequence of REAL st
( rng b1 c= A & b1 . (len b1) = upper_bound A ) by A6, A5; :: thesis: verum