theorem :: RCOMP_3:49

for r, s being Real
for F being Subset-Family of (Closed-Interval-TSpace (r,s)) st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & [.r,s.] in F holds
<*[.r,s.]*> is IntervalCover of F