let r, s be real number ; :: thesis: for n being natural number
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 natural number ; :: 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 )
assume that
A1: F is Cover of (Closed-Interval-TSpace r,s) and
A2: F is open and
A3: F is connected and
A4: r <= s ; :: thesis: ( not 1 < n or not n <= len C or lower_bound (C /. n) < G . n )
set w = n -' 1;
assume that
A5: 1 < n and
A6: n <= len C ; :: thesis: lower_bound (C /. n) < G . n
A7: len G = (len C) + 1 by A1, A2, A3, A4, Def3;
1 - 1 <= n - 1 by A5, XREAL_1:11;
then A8: n -' 1 = n - 1 by XREAL_0:def 2;
then n = (n -' 1) + 1 ;
then A9: 1 <= n -' 1 by A5, NAT_1:13;
n < (len C) + 1 by A6, NAT_1:13;
then G . ((n -' 1) + 1) in ].(lower_bound (C /. ((n -' 1) + 1))),(upper_bound (C /. (n -' 1))).[ by A1, A2, A3, A4, A7, A8, A9, Def3;
hence lower_bound (C /. n) < G . n by A8, XXREAL_1:4; :: thesis: verum