let r, s be Real; :: thesis: for n being Nat
for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 < n & n <= len C holds
lower_bound (C /. n) < G . n
let n be Nat; :: thesis: for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 < n & n <= len C holds
lower_bound (C /. n) < G . n
let F be Subset-Family of (Closed-Interval-TSpace (r,s)); :: thesis: for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 < n & n <= len C holds
lower_bound (C /. n) < G . n
let C be IntervalCover of F; :: thesis: for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 < n & n <= len C holds
lower_bound (C /. n) < G . n
let G be IntervalCoverPts of C; :: thesis: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 < n & n <= len C implies lower_bound (C /. n) < G . n )
set w = n -' 1;
assume A1: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s ) ; :: thesis: ( not 1 < n or not n <= len C or lower_bound (C /. n) < G . n )
then A2: len G = (len C) + 1 by Def3;
assume that
A3: 1 < n and
A4: n <= len C ; :: thesis: lower_bound (C /. n) < G . n
A5: n < (len C) + 1 by A4, NAT_1:13;
1 - 1 <= n - 1 by A3, XREAL_1:9;
then A6: n -' 1 = n - 1 by XREAL_0:def 2;
then n = (n -' 1) + 1 ;
then 1 <= n -' 1 by A3, NAT_1:13;
then G . ((n -' 1) + 1) in ].(lower_bound (C /. ((n -' 1) + 1))),(upper_bound (C /. (n -' 1))).[ by A1, A2, A6, A5, Def3;
hence lower_bound (C /. n) < G . n by A6, XXREAL_1:4; :: thesis: verum