theorem Th55: :: RCOMP_3:55

for r, s being Real
for n being Nat
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 & 1 <= n & n + 1 <= len C holds
not ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ is empty