let r, s be Real; :: thesis: 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.[ ) ) ) ) )
let jauge be Function of [.r,s.],].0,+infty.[; :: thesis: 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.[ ) ) ) ) )
let S be Subset-Family of (Closed-Interval-TSpace (r,s)); :: thesis: ( r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } implies 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.[ ) ) ) ) ) )
assume that
A1: r <= s and
A2: S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } ; :: thesis: 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.[ ) ) ) ) )
let IC be IntervalCover of S; :: thesis: ( 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.[ ) ) ) ) )
( S is Subset-Family of (Closed-Interval-TSpace (r,s)) & S is Cover of (Closed-Interval-TSpace (r,s)) & S is open & S is connected & r <= s ) by A1, A2, Th39, Th40, Th41;
hence ( 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.[ ) ) ) ) ) by RCOMP_3:def 2; :: thesis: verum