let r, s be Real; 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 + 1 < len G holds
G . (n + 1) < upper_bound (C /. n)
let n be 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 + 1 < len G holds
G . (n + 1) < upper_bound (C /. n)
let F be 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 C be 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 G be IntervalCoverPts of C; ( 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
( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n + 1 < len G )
; G . (n + 1) < upper_bound (C /. n)
then
G . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[
by Def3;
hence
G . (n + 1) < upper_bound (C /. n)
by XXREAL_1:4; verum