let r be Real; :: 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:18;
then r in the carrier of (Closed-Interval-TSpace (r,r)) by A3, TARSKI:def 1;
then {r} in F by A1, Th46;
hence C = <*[.r,r.]*> by A1, A2, A3, Def2; :: thesis: verum