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 + 1 < len G holds
G . (n + 1) < upper_bound (C /. 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 + 1 < len G holds
G . (n + 1) < upper_bound (C /. 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 + 1 < len G holds
G . (n + 1) < upper_bound (C /. 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 + 1 < len G holds
G . (n + 1) < upper_bound (C /. 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 + 1 < len G implies G . (n + 1) < upper_bound (C /. 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 and
A5: 1 <= n and
A6: n + 1 < len G ; :: thesis: G . (n + 1) < upper_bound (C /. n)
G . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ by A1, A2, A3, A4, A5, A6, Def3;
hence G . (n + 1) < upper_bound (C /. n) by XXREAL_1:4; :: thesis: verum