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 holds
s in C /. (len C)
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 holds
s in C /. (len C)
let C be IntervalCover of F; :: thesis: ( F is Cover of (Closed-Interval-TSpace r,s) & F is open & F is connected & r <= s implies s in C /. (len C) )
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 ; :: thesis: s in C /. (len C)
1 <= len C by A1, A2, A3, A4, Th65;
then A5: C . (len C) = C /. (len C) by FINSEQ_4:24;

per cases ( [.r,s.] in F or not [.r,s.] in F ) ;

suppose [.r,s.] in F ; :: thesis: s in C /. (len C)

then A6: C = <*[.r,s.]*> by A1, A2, A3, A4, Def2;
then A7: C /. 1 = [.r,s.] by FINSEQ_4:25;
len C = 1 by A6, FINSEQ_1:56;
hence s in C /. (len C) by A4, A7, XXREAL_1:1; :: thesis: verum

end;

suppose not [.r,s.] in F ; :: thesis: s in C /. (len C)

then ex p being real number st
( r <= p & p < s & C . (len C) = ].p,s.] ) by A1, A2, A3, A4, Def2;
hence s in C /. (len C) by A5, XXREAL_1:2; :: thesis: verum

end;

end;