let r, s be Real; :: thesis: for n, m being Nat
for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & n in dom C & m in dom C & n < m holds
upper_bound (C /. n) <= upper_bound (C /. m)
let n, m be Nat; :: thesis: for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & n in dom C & m in dom C & n < m holds
upper_bound (C /. n) <= upper_bound (C /. m)
let F be Subset-Family of (Closed-Interval-TSpace (r,s)); :: thesis: for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & n in dom C & m in dom C & n < m holds
upper_bound (C /. n) <= upper_bound (C /. m)
let C be IntervalCover of F; :: thesis: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & n in dom C & m in dom C & n < m implies upper_bound (C /. n) <= upper_bound (C /. m) )
assume that
A1: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s ) and
A2: n in dom C and
A3: ( m in dom C & n < m ) ; :: thesis: upper_bound (C /. n) <= upper_bound (C /. m)
defpred S₂[ Nat] means ( $1 in dom C & n < $1 implies upper_bound (C /. n) <= upper_bound (C /. $1) );
A4: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume that
A5: S₂[k] and
A6: k + 1 in dom C and
A7: n < k + 1 ; :: thesis: upper_bound (C /. n) <= upper_bound (C /. (k + 1))

per cases ( k = 0 or k in dom C ) by A6, TOPREALA:2;

suppose k = 0 ; :: thesis: upper_bound (C /. n) <= upper_bound (C /. (k + 1))

then n = 0 by A7, NAT_1:13;
hence upper_bound (C /. n) <= upper_bound (C /. (k + 1)) by A2, FINSEQ_3:24; :: thesis: verum

end;

suppose A8: k in dom C ; :: thesis: upper_bound (C /. n) <= upper_bound (C /. (k + 1))

A9: k + 1 <= len C by A6, FINSEQ_3:25;
A10: n <= k by A7, NAT_1:13;
1 <= k by A8, FINSEQ_3:25;
then upper_bound (C /. k) <= upper_bound (C /. (k + 1)) by A1, A9, Def2;
hence upper_bound (C /. n) <= upper_bound (C /. (k + 1)) by A5, A8, A10, XXREAL_0:1, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A11: S₂[ 0 ] ;
for k being Nat holds S₂[k] from NAT_1:sch 2(A11, A4);
hence upper_bound (C /. n) <= upper_bound (C /. m) by A3; :: thesis: verum