theorem :: RCOMP_3:54

for r, s being Real
for n, m 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 & n in dom C & m in dom C & n < m holds
upper_bound (C /. n) <= upper_bound (C /. m)