theorem :: COUSIN:57

for r, s being Real
for jauge being Function of [.r,s.],].0,+infty.[
for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
for IC being IntervalCover of S holds
( IC is FinSequence of bool REAL & rng IC c= S & union (rng IC) = [.r,s.] & ( for n being Nat st 1 <= n holds
( ( n <= len IC implies not IC /. n is empty ) & ( n + 1 <= len IC implies ( lower_bound (IC /. n) <= lower_bound (IC /. (n + 1)) & upper_bound (IC /. n) <= upper_bound (IC /. (n + 1)) & lower_bound (IC /. (n + 1)) < upper_bound (IC /. n) ) ) & ( n + 2 <= len IC implies upper_bound (IC /. n) <= lower_bound (IC /. (n + 2)) ) ) ) & ( [.r,s.] in S implies IC = <*[.r,s.]*> ) & ( not [.r,s.] in S implies ( ex p being Real st
( r < p & p <= s & IC . 1 = [.r,p.[ ) & ex p being Real st
( r <= p & p < s & IC . (len IC) = ].p,s.] ) & ( for n being Nat st 1 < n & n < len IC holds
ex p, q being Real st
( r <= p & p < q & q <= s & IC . n = ].p,q.[ ) ) ) ) )