consider a being Element of REAL such that
A1: a = upper_bound A ;
reconsider p = (Seg 1) --> a as Function of (Seg 1),REAL by FUNCOP_1:57;
A2: dom p = Seg 1 by FUNCOP_1:19;
reconsider p = p as FinSequence ;
rng p c= REAL by RELAT_1:def 19;
then reconsider p = p as FinSequence of REAL by FINSEQ_1:def 4;
A3: 1 in Seg 1 by FINSEQ_1:4, TARSKI:def 1;
for n, m being Element of NAT st n in dom p & m in dom p & n < m holds
p . n < p . m

proof

let n, m be Element of NAT ; :: thesis: ( n in dom p & m in dom p & n < m implies p . n < p . m )
assume that
A4: n in dom p and
A5: m in dom p ; :: thesis: ( not n < m or p . n < p . m )
n = 1 by A2, A4, FINSEQ_1:4, TARSKI:def 1;
hence ( not n < m or p . n < p . m ) by A2, A5, FINSEQ_1:4, TARSKI:def 1; :: thesis: verum

end;

then A6: p is non empty increasing FinSequence of REAL by SEQM_3:def 1;
upper_bound A in A by RCOMP_1:32;
then for n being Nat st n in Seg 1 holds
p . n in A by A1, FUNCOP_1:13;
then p is FinSequence of A by A2, FINSEQ_2:14;
then A7: rng p c= A by FINSEQ_1:def 4;
len p = 1 by A2, FINSEQ_1:def 3;
then p . (len p) = upper_bound A by A1, A3, FUNCOP_1:13;
hence ex b₁ being non empty increasing FinSequence of REAL st
( rng b₁ c= A & b₁ . (len b₁) = upper_bound A ) by A7, A6; :: thesis: verum