:: deftheorem Def2 defines IntervalCover RCOMP_3:def 2 :
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 holds
for b₄ being FinSequence of bool REAL holds
( b₄ is IntervalCover of F iff ( rng b₄ c= F & union (rng b₄) = [.r,s.] & ( for n being Nat st 1 <= n holds
( ( n <= len b₄ implies not b₄ /. n is empty ) & ( n + 1 <= len b₄ implies ( lower_bound (b₄ /. n) <= lower_bound (b₄ /. (n + 1)) & upper_bound (b₄ /. n) <= upper_bound (b₄ /. (n + 1)) & lower_bound (b₄ /. (n + 1)) < upper_bound (b₄ /. n) ) ) & ( n + 2 <= len b₄ implies upper_bound (b₄ /. n) <= lower_bound (b₄ /. (n + 2)) ) ) ) & ( [.r,s.] in F implies b₄ = <*[.r,s.]*> ) & ( not [.r,s.] in F implies ( ex p being Real st
( r < p & p <= s & b₄ . 1 = [.r,p.[ ) & ex p being Real st
( r <= p & p < s & b₄ . (len b₄) = ].p,s.] ) & ( for n being Nat st 1 < n & n < len b₄ holds
ex p, q being Real st
( r <= p & p < q & q <= s & b₄ . n = ].p,q.[ ) ) ) ) ) );