set A = (len C) + 1;
defpred S2[ Nat, set ] means ( ( $1 = 1 implies $2 = r ) & ( $1 = (len C) + 1 implies $2 = s ) & ( 2 <= $1 & $1 <= len C implies $2 in ].(lower_bound (C /. $1)),(upper_bound (C /. ($1 - 1))).[ ) );
A2: 0 + 1 <= len C by A1, Th51;
then A3: 0 + 1 < (len C) + 1 by XREAL_1:6;
A4: for k being Nat st k in Seg ((len C) + 1) holds
ex x being Element of REAL st S2[k,x]
proof
reconsider r = r, s = s as Element of REAL by XREAL_0:def 1;
let k be Nat; :: thesis: ( k in Seg ((len C) + 1) implies ex x being Element of REAL st S2[k,x] )
A5: (len C) + 0 < (len C) + 1 by XREAL_1:6;
assume k in Seg ((len C) + 1) ; :: thesis: ex x being Element of REAL st S2[k,x]
then A6: ( 1 <= k & k <= (len C) + 1 ) by FINSEQ_1:1;
per cases ( k = 1 or k = (len C) + 1 or ( 1 < k & k < (len C) + 1 ) ) by A6, XXREAL_0:1;
suppose A7: k = 1 ; :: thesis: ex x being Element of REAL st S2[k,x]
take r ; :: thesis: S2[k,r]
thus S2[k,r] by A2, A7; :: thesis: verum
end;
suppose A8: k = (len C) + 1 ; :: thesis: ex x being Element of REAL st S2[k,x]
take s ; :: thesis: S2[k,s]
thus S2[k,s] by A2, A5, A8; :: thesis: verum
end;
suppose that A9: 1 < k and
A10: k < (len C) + 1 ; :: thesis: ex x being Element of REAL st S2[k,x]
A11: k - 1 in NAT by A9, INT_1:5;
A12: k <= len C by A10, NAT_1:13;
1 - 1 < k - 1 by A9, XREAL_1:14;
then 0 + 1 <= k - 1 by A11, NAT_1:13;
then not ].(lower_bound (C /. ((k - 1) + 1))),(upper_bound (C /. (k - 1))).[ is empty by A1, A11, A12, Th55;
then consider x being object such that
A13: x in ].(lower_bound (C /. ((k - 1) + 1))),(upper_bound (C /. (k - 1))).[ ;
reconsider x = x as Real by A13;
take x ; :: thesis: ( x is set & x is Element of REAL & S2[k,x] )
thus ( x is set & x is Element of REAL & S2[k,x] ) by A9, A10, A13; :: thesis: verum
end;
end;
end;
consider p being FinSequence of REAL such that
A14: dom p = Seg ((len C) + 1) and
A15: for k being Nat st k in Seg ((len C) + 1) holds
S2[k,p . k] from FINSEQ_1:sch 5(A4);
 take p ; :: thesis: ( len p = (len C) + 1 & p . 1 = r & p . (len p) = s & ( for n being Nat st 1 <= n & n + 1 < len p holds
p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) )
thus A16: len p = (len C) + 1 by A14, FINSEQ_1:def 3; :: thesis: ( p . 1 = r & p . (len p) = s & ( for n being Nat st 1 <= n & n + 1 < len p holds
p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) )
1 in Seg ((len C) + 1) by A3, FINSEQ_1:1;
hence p . 1 = r by A15; :: thesis: ( p . (len p) = s & ( for n being Nat st 1 <= n & n + 1 < len p holds
p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) )
len p in Seg ((len C) + 1) by A3, A16, FINSEQ_1:1;
hence p . (len p) = s by A15, A16; :: thesis: for n being Nat st 1 <= n & n + 1 < len p holds
p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[
let n be Nat; :: thesis: ( 1 <= n & n + 1 < len p implies p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ )
assume 1 <= n ; :: thesis: ( not n + 1 < len p or p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ )
then A17: 1 + 1 <= n + 1 by XREAL_1:6;
assume A18: n + 1 < len p ; :: thesis: p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[
0 + 1 <= n + 1 by XREAL_1:6;
then A19: n + 1 in Seg ((len C) + 1) by A16, A18, FINSEQ_1:1;
n + 1 <= len C by A16, A18, NAT_1:13;
then p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. ((n + 1) - 1))).[ by A15, A19, A17;
hence p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ; :: thesis: verum