let r, s be real number ; :: thesis: for F being Subset-Family of (Closed-Interval-TSpace r,s) st F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s & [.r,s.] in F holds
<*[.r,s.]*> is IntervalCover of F
let F be Subset-Family of (Closed-Interval-TSpace r,s); :: thesis: ( F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s & [.r,s.] in F implies <*[.r,s.]*> is IntervalCover of F )
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: [.r,s.] in F ; :: thesis: <*[.r,s.]*> is IntervalCover of F
set f = <*[.r,s.]*>;
( rng <*[.r,s.]*> c= F & union (rng <*[.r,s.]*>) = [.r,s.] & ( for n being natural number st 1 <= n holds
( ( n <= len <*[.r,s.]*> implies not <*[.r,s.]*> /. n is empty ) & ( n + 1 <= len <*[.r,s.]*> implies ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) ) ) & ( n + 2 <= len <*[.r,s.]*> implies upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) ) ) ) ) by A4, A5, Lm4;
hence <*[.r,s.]*> is IntervalCover of F by A1, A2, A3, A4, A5, Def2; :: thesis: verum