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))).[ ) );
A1: 0 + 1 <= len C by B1, Th51;
then A2: 0 + 1 < (len C) + 1 by XREAL_1:6;
A3: 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 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] )
A4: (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 A5: ( 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 A5, XXREAL_0:1;
suppose A6: k = 1 ; :: thesis: ex x being Element of REAL st S2[k,x]
take r ; :: thesis: S2[k,r]
thus S2[k,r] by A1, A6; :: thesis: verum
end;
suppose A7: 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 A1, A4, A7; :: thesis: verum
end;
suppose that A8: 1 < k and
A9: k < (len C) + 1 ; :: thesis: ex x being Element of REAL st S2[k,x]
A10: k - 1 in NAT by A8, INT_1:5;
A11: k <= len C by A9, NAT_1:13;
1 - 1 < k - 1 by A8, XREAL_1:14;
then 0 + 1 <= k - 1 by A10, NAT_1:13;
then not ].(lower_bound (C /. ((k - 1) + 1))),(upper_bound (C /. (k - 1))).[ is empty by B1, A10, A11, Th55;
then consider x being set such that
A12: x in ].(lower_bound (C /. ((k - 1) + 1))),(upper_bound (C /. (k - 1))).[ by XBOOLE_0:def 1;
reconsider x = x as Real by A12;
take x ; :: thesis: S2[k,x]
thus S2[k,x] by A8, A9, A12; :: thesis: verum
end;
end;
end;
consider p being FinSequence of REAL such that
A13: dom p = Seg ((len C) + 1) and
A14: for k being Nat st k in Seg ((len C) + 1) holds
S2[k,p . k] from FINSEQ_1:sch 5(A3);
 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 A15: len p = (len C) + 1 by A13, 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 A2, FINSEQ_1:1;
hence p . 1 = r by A14; :: 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 A2, A15, FINSEQ_1:1;
hence p . (len p) = s by A14, A15; :: 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 A16: 1 + 1 <= n + 1 by XREAL_1:6;
assume A17: 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 A18: n + 1 in Seg ((len C) + 1) by A15, A17, FINSEQ_1:1;
n + 1 <= len C by A15, A17, NAT_1:13;
then p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. ((n + 1) - 1))).[ by A14, A18, A16;
hence p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ; :: thesis: verum