let r, s be Real; :: thesis:
let n, m be Nat; :: thesis:
let F be Subset-Family of (Closed-Interval-TSpace (r,s)); :: thesis:
let C be IntervalCover of F; :: thesis:
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:
defpred S₂[ Nat] means ( $1 in dom C & n < $1 implies lower_bound (C /. n) <= lower_bound (C /. $1) );
A4: for k being Nat st S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis:
assume that
A5: S₂[k] and
A6: k + 1 in dom C and
A7: n < k + 1 ; :: thesis:

per cases by A6, TOPREALA:2;

suppose k = 0 ; :: thesis:

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

end;

suppose A8: k in dom C ; :: thesis:

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 lower_bound (C /. k) <= lower_bound (C /. (k + 1)) by A1, A9, Def2;
hence lower_bound (C /. n) <= lower_bound (C /. (k + 1)) by A5, A8, A10, XXREAL_0:1, XXREAL_0:2; :: thesis:

end;

end;

end;

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