let r, s be Real; :: 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
upper_bound (C /. (len C)) = 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 holds
upper_bound (C /. (len C)) = 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 implies upper_bound (C /. (len C)) = s )
assume that
A1: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected ) and
A2: r <= s ; :: thesis: upper_bound (C /. (len C)) = s
1 <= len C by A1, A2, Th51;
then A3: C . (len C) = C /. (len C) by FINSEQ_4:15;

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

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

then C = <*[.r,s.]*> by A1, A2, Def2;
then ( C /. 1 = [.r,s.] & len C = 1 ) by FINSEQ_1:39, FINSEQ_4:16;
hence upper_bound (C /. (len C)) = s by A2, JORDAN5A:19; :: thesis: verum

end;

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

then ex p being Real st
( r <= p & p < s & C . (len C) = ].p,s.] ) by A1, A2, Def2;
hence upper_bound (C /. (len C)) = s by A3, Th7; :: thesis: verum

end;

end;