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 st F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s & 1 <= n & n + 1 <= len C holds
not ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ is empty
let n be natural number ; :: 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 & 1 <= n & n + 1 <= len C holds
not ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ is empty
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 & 1 <= n & n + 1 <= len C holds
not ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ is empty
let C be IntervalCover of F; :: thesis: ( F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s & 1 <= n & n + 1 <= len C implies not ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ is empty )
assume ( F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s & 1 <= n & n + 1 <= len C ) ; :: thesis: not ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ is empty
then lower_bound (C /. (n + 1)) < upper_bound (C /. n) by Def2;
hence not ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ is empty by XXREAL_1:33; :: thesis: verum