let r, s be real number ; :: thesis: for F being Subset-Family of (Closed-Interval-TSpace r,s)
for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s & len C = 1 holds
C = <*[.r,s.]*>
let F be Subset-Family of (Closed-Interval-TSpace r,s); :: thesis: for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s & len C = 1 holds
C = <*[.r,s.]*>
let C be IntervalCover of F; :: thesis: ( F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s & len C = 1 implies C = <*[.r,s.]*> )
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: len C = 1 ; :: thesis: C = <*[.r,s.]*>
A6: union (rng C) = [.r,s.] by A1, A2, A3, A4, Def2;
not C is empty by A5;
then not rng C is empty ;
then 1 in dom C by FINSEQ_3:34;
then A7: C . 1 in rng C by FUNCT_1:def 5;
C . 1 = [.r,s.]

proof

thus for a being set st a in C . 1 holds
a in [.r,s.] by A6, A7, TARSKI:def 4; :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [.r,s.] c= C . 1
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in [.r,s.] or a in C . 1 )
assume a in [.r,s.] ; :: thesis: a in C . 1
then consider Z being set such that
A8: a in Z and
A9: Z in rng C by A6, TARSKI:def 4;
A10: ex x being set st
( x in dom C & C . x = Z ) by A9, FUNCT_1:def 5;
dom C = {1} by A5, FINSEQ_1:4, FINSEQ_1:def 3;
hence a in C . 1 by A8, A10, TARSKI:def 1; :: thesis: verum

end;

hence C = <*[.r,s.]*> by A5, FINSEQ_1:57; :: thesis: verum