let r be real number ; :: thesis: for F being Subset-Family of (Closed-Interval-TSpace r,r)
for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace r,r) & F is open & F is connected holds
C = <*[.r,r.]*>
set L = Closed-Interval-TSpace r,r;
let F be Subset-Family of (Closed-Interval-TSpace r,r); :: thesis: for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace r,r) & F is open & F is connected holds
C = <*[.r,r.]*>
let C be IntervalCover of F; :: thesis: ( F is Cover of (Closed-Interval-TSpace r,r) & F is open & F is connected implies C = <*[.r,r.]*> )
assume that
A1: F is Cover of (Closed-Interval-TSpace r,r) and
A2: ( F is open & F is connected ) ; :: thesis: C = <*[.r,r.]*>
A3: [.r,r.] = {r} by XXREAL_1:17;
the carrier of (Closed-Interval-TSpace r,r) = [.r,r.] by TOPMETR:25;
then r in the carrier of (Closed-Interval-TSpace r,r) by A3, TARSKI:def 1;
then {r} in F by A1, Th60;
hence C = <*[.r,r.]*> by A1, A2, A3, Def2; :: thesis: verum