theorem Th64: :: RCOMP_3:64

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
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len C holds
G . n <= lower_bound (C /. (n + 1))