:: deftheorem Def3 defines IntervalCoverPts RCOMP_3:def 3 :
for r, s being Real
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
for b₅ being FinSequence of REAL holds
( b₅ is IntervalCoverPts of C iff ( len b₅ = (len C) + 1 & b₅ . 1 = r & b₅ . (len b₅) = s & ( for n being Nat st 1 <= n & n + 1 < len b₅ holds
b₅ . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) ) );