:: Properties of Connected Subsets of the Real Line :: by Artur Korni{\l}owicz :: :: Received February 22, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin registration let X be non empty set ; cluster [#] X -> non empty ; coherence not [#] X is empty ; end; registration cluster -> real-membered for SubSpace of RealSpace ; coherence for b1 being SubSpace of RealSpace holds b1 is real-membered proofend; end; theorem Th1: :: RCOMP_3:1 for X being non empty real-membered bounded_below set for Y being closed Subset of REAL st X c= Y holds lower_bound X in Y proofend; theorem Th2: :: RCOMP_3:2 for X being non empty real-membered bounded_above set for Y being closed Subset of REAL st X c= Y holds upper_bound X in Y proofend; theorem Th3: :: RCOMP_3:3 for X, Y being Subset of REAL holds Cl (X \/ Y) = (Cl X) \/ (Cl Y) proofend; begin registration let r be real number ; let s be ext-real number ; cluster[.r,s.[ -> bounded_below ; coherence [.r,s.[ is bounded_below proofend; cluster].s,r.] -> bounded_above ; coherence ].s,r.] is bounded_above proofend; end; registration let r, s be real number ; cluster[.r,s.[ -> real-bounded ; coherence [.r,s.[ is real-bounded proofend; cluster].r,s.] -> real-bounded ; coherence ].r,s.] is real-bounded proofend; cluster].r,s.[ -> real-bounded ; coherence ].r,s.[ is real-bounded proofend; end; registration cluster non empty complex-membered ext-real-membered real-membered open real-bounded interval for Element of K32(REAL); existence ex b1 being Subset of REAL st ( b1 is open & b1 is real-bounded & b1 is interval & not b1 is empty ) proofend; end; theorem Th4: :: RCOMP_3:4 for r, s being real number st r < s holds lower_bound [.r,s.[ = r proofend; theorem Th5: :: RCOMP_3:5 for r, s being real number st r < s holds upper_bound [.r,s.[ = s proofend; theorem Th6: :: RCOMP_3:6 for r, s being real number st r < s holds lower_bound ].r,s.] = r proofend; theorem Th7: :: RCOMP_3:7 for r, s being real number st r < s holds upper_bound ].r,s.] = s proofend; begin theorem Th8: :: RCOMP_3:8 for a, b being real number st a <= b holds [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b} proofend; Lm1: now__::_thesis:_for_a_being_real_number_holds_not_left_open_halfline_a_is_bounded_below let a be real number ; ::_thesis: not left_open_halfline a is bounded_below assume left_open_halfline a is bounded_below ; ::_thesis: contradiction then consider b being real number such that A1: b is LowerBound of left_open_halfline a by XXREAL_2:def_9; A2: for r being real number st r in left_open_halfline a holds b <= r by A1, XXREAL_2:def_2; A3: a - 1 < a - 0 by XREAL_1:15; then a - 1 in left_open_halfline a by XXREAL_1:233; then b - 1 < (a - 1) - 0 by A2, XREAL_1:15; then b - 1 < a by A3, XXREAL_0:2; then b - 1 in left_open_halfline a by XXREAL_1:233; then b - 0 <= b - 1 by A1, XXREAL_2:def_2; hence contradiction by XREAL_1:15; ::_thesis: verum end; Lm2: now__::_thesis:_for_a_being_real_number_holds_not_right_open_halfline_a_is_bounded_above let a be real number ; ::_thesis: not right_open_halfline a is bounded_above assume right_open_halfline a is bounded_above ; ::_thesis: contradiction then consider b being real number such that A1: b is UpperBound of right_open_halfline a by XXREAL_2:def_10; A2: a + 0 < a + 1 by XREAL_1:6; then a + 1 in right_open_halfline a by XXREAL_1:235; then a + 1 <= b by A1, XXREAL_2:def_1; then (a + 1) + 0 <= b + 1 by XREAL_1:7; then a < b + 1 by A2, XXREAL_0:2; then b + 1 in right_open_halfline a by XXREAL_1:235; then b + 1 <= b + 0 by A1, XXREAL_2:def_1; hence contradiction by XREAL_1:6; ::_thesis: verum end; registration let a be real number ; cluster left_closed_halfline a -> non bounded_below bounded_above interval ; coherence ( not left_closed_halfline a is bounded_below & left_closed_halfline a is bounded_above & left_closed_halfline a is interval ) proofend; cluster left_open_halfline a -> non bounded_below bounded_above interval ; coherence ( not left_open_halfline a is bounded_below & left_open_halfline a is bounded_above & left_open_halfline a is interval ) proofend; cluster right_closed_halfline a -> bounded_below non bounded_above interval ; coherence ( right_closed_halfline a is bounded_below & not right_closed_halfline a is bounded_above & right_closed_halfline a is interval ) proofend; cluster right_open_halfline a -> bounded_below non bounded_above interval ; coherence ( right_open_halfline a is bounded_below & not right_open_halfline a is bounded_above & right_open_halfline a is interval ) proofend; end; theorem Th9: :: RCOMP_3:9 for a being real number holds upper_bound (left_closed_halfline a) = a proofend; theorem Th10: :: RCOMP_3:10 for a being real number holds upper_bound (left_open_halfline a) = a proofend; theorem Th11: :: RCOMP_3:11 for a being real number holds lower_bound (right_closed_halfline a) = a proofend; theorem Th12: :: RCOMP_3:12 for a being real number holds lower_bound (right_open_halfline a) = a proofend; begin registration cluster [#] REAL -> non bounded_below non bounded_above interval ; coherence ( [#] REAL is interval & not [#] REAL is bounded_below & not [#] REAL is bounded_above ) ; end; theorem Th13: :: RCOMP_3:13 for X being real-bounded interval Subset of REAL st lower_bound X in X & upper_bound X in X holds X = [.(lower_bound X),(upper_bound X).] proofend; theorem Th14: :: RCOMP_3:14 for X being real-bounded Subset of REAL st not lower_bound X in X holds X c= ].(lower_bound X),(upper_bound X).] proofend; theorem Th15: :: RCOMP_3:15 for X being real-bounded interval Subset of REAL st not lower_bound X in X & upper_bound X in X holds X = ].(lower_bound X),(upper_bound X).] proofend; theorem Th16: :: RCOMP_3:16 for X being real-bounded Subset of REAL st not upper_bound X in X holds X c= [.(lower_bound X),(upper_bound X).[ proofend; theorem Th17: :: RCOMP_3:17 for X being real-bounded interval Subset of REAL st lower_bound X in X & not upper_bound X in X holds X = [.(lower_bound X),(upper_bound X).[ proofend; theorem Th18: :: RCOMP_3:18 for X being real-bounded Subset of REAL st not lower_bound X in X & not upper_bound X in X holds X c= ].(lower_bound X),(upper_bound X).[ proofend; theorem Th19: :: RCOMP_3:19 for X being non empty real-bounded interval Subset of REAL st not lower_bound X in X & not upper_bound X in X holds X = ].(lower_bound X),(upper_bound X).[ proofend; theorem Th20: :: RCOMP_3:20 for X being Subset of REAL st X is bounded_above holds X c= left_closed_halfline (upper_bound X) proofend; theorem Th21: :: RCOMP_3:21 for X being interval Subset of REAL st not X is bounded_below & X is bounded_above & upper_bound X in X holds X = left_closed_halfline (upper_bound X) proofend; theorem Th22: :: RCOMP_3:22 for X being Subset of REAL st X is bounded_above & not upper_bound X in X holds X c= left_open_halfline (upper_bound X) proofend; theorem Th23: :: RCOMP_3:23 for X being non empty interval Subset of REAL st not X is bounded_below & X is bounded_above & not upper_bound X in X holds X = left_open_halfline (upper_bound X) proofend; theorem Th24: :: RCOMP_3:24 for X being Subset of REAL st X is bounded_below holds X c= right_closed_halfline (lower_bound X) proofend; theorem Th25: :: RCOMP_3:25 for X being interval Subset of REAL st X is bounded_below & not X is bounded_above & lower_bound X in X holds X = right_closed_halfline (lower_bound X) proofend; theorem Th26: :: RCOMP_3:26 for X being Subset of REAL st X is bounded_below & not lower_bound X in X holds X c= right_open_halfline (lower_bound X) proofend; theorem Th27: :: RCOMP_3:27 for X being non empty interval Subset of REAL st X is bounded_below & not X is bounded_above & not lower_bound X in X holds X = right_open_halfline (lower_bound X) proofend; theorem Th28: :: RCOMP_3:28 for X being interval Subset of REAL st not X is bounded_above & not X is bounded_below holds X = REAL proofend; theorem Th29: :: RCOMP_3:29 for X being interval Subset of REAL holds ( X is empty or X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st ( a <= b & X = [.a,b.] ) or ex a, b being real number st ( a < b & X = [.a,b.[ ) or ex a, b being real number st ( a < b & X = ].a,b.] ) or ex a, b being real number st ( a < b & X = ].a,b.[ ) ) proofend; theorem Th30: :: RCOMP_3:30 for r being real number for X being non empty interval Subset of REAL holds ( r in X or r <= lower_bound X or upper_bound X <= r ) proofend; theorem Th31: :: RCOMP_3:31 for X, Y being non empty real-bounded interval Subset of REAL st lower_bound X <= lower_bound Y & upper_bound Y <= upper_bound X & ( lower_bound X = lower_bound Y & lower_bound Y in Y implies lower_bound X in X ) & ( upper_bound X = upper_bound Y & upper_bound Y in Y implies upper_bound X in X ) holds Y c= X proofend; registration cluster non empty complex-membered ext-real-membered real-membered closed open non real-bounded interval for Element of K32(REAL); existence ex b1 being Subset of REAL st ( b1 is open & b1 is closed & b1 is interval & not b1 is empty & not b1 is real-bounded ) proofend; end; begin theorem Th32: :: RCOMP_3:32 for a, b being real number for X being Subset of R^1 st a <= b & X = [.a,b.] holds Fr X = {a,b} proofend; theorem :: RCOMP_3:33 for a, b being real number for X being Subset of R^1 st a < b & X = ].a,b.[ holds Fr X = {a,b} proofend; theorem Th34: :: RCOMP_3:34 for a, b being real number for X being Subset of R^1 st a < b & X = [.a,b.[ holds Fr X = {a,b} proofend; theorem Th35: :: RCOMP_3:35 for a, b being real number for X being Subset of R^1 st a < b & X = ].a,b.] holds Fr X = {a,b} proofend; theorem :: RCOMP_3:36 for a, b being real number for X being Subset of R^1 st X = [.a,b.] holds Int X = ].a,b.[ proofend; theorem :: RCOMP_3:37 for a, b being real number for X being Subset of R^1 st X = ].a,b.[ holds Int X = ].a,b.[ proofend; theorem Th38: :: RCOMP_3:38 for a, b being real number for X being Subset of R^1 st X = [.a,b.[ holds Int X = ].a,b.[ proofend; theorem Th39: :: RCOMP_3:39 for a, b being real number for X being Subset of R^1 st X = ].a,b.] holds Int X = ].a,b.[ proofend; registration let T be real-membered TopStruct ; let X be interval Subset of T; clusterT | X -> interval ; coherence T | X is interval proofend; end; registration let A be interval Subset of REAL; cluster R^1 A -> interval ; coherence R^1 A is interval by TOPREALB:def_3; end; registration cluster connected -> interval for Element of K32( the carrier of R^1); coherence for b1 being Subset of R^1 st b1 is connected holds b1 is interval proofend; cluster interval -> connected for Element of K32( the carrier of R^1); coherence for b1 being Subset of R^1 st b1 is interval holds b1 is connected proofend; end; begin registration let r be real number ; cluster Closed-Interval-TSpace (r,r) -> 1 -element ; coherence Closed-Interval-TSpace (r,r) is 1 -element proofend; end; theorem :: RCOMP_3:40 for r, s being real number st r <= s holds for A being Subset of (Closed-Interval-TSpace (r,s)) holds A is real-bounded Subset of REAL proofend; theorem Th41: :: RCOMP_3:41 for r, s, a, b being real number st r <= s holds for X being Subset of (Closed-Interval-TSpace (r,s)) st X = [.a,b.[ & r < a & b <= s holds Int X = ].a,b.[ proofend; theorem Th42: :: RCOMP_3:42 for r, s, a, b being real number st r <= s holds for X being Subset of (Closed-Interval-TSpace (r,s)) st X = ].a,b.] & r <= a & b < s holds Int X = ].a,b.[ proofend; theorem Th43: :: RCOMP_3:43 for r, s being real number for X being Subset of (Closed-Interval-TSpace (r,s)) for Y being Subset of REAL st X = Y holds ( X is connected iff Y is interval ) proofend; registration let T be TopSpace; cluster open closed connected for Element of K32( the carrier of T); existence ex b1 being Subset of T st ( b1 is open & b1 is closed & b1 is connected ) proofend; end; registration let T be non empty connected TopSpace; cluster non empty open closed connected for Element of K32( the carrier of T); existence ex b1 being Subset of T st ( not b1 is empty & b1 is open & b1 is closed & b1 is connected ) proofend; end; theorem Th44: :: RCOMP_3:44 for r, s being real number st r <= s holds for X being open connected Subset of (Closed-Interval-TSpace (r,s)) holds ( X is empty or X = [.r,s.] or ex a being real number st ( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st ( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st ( r <= a & a < b & b <= s & X = ].a,b.[ ) ) proofend; begin deffunc H1( set ) -> set = $1; defpred S1[ set , set ] means $1 c= $2; theorem Th45: :: RCOMP_3:45 for T being 1-sorted for F being finite Subset-Family of T for F1 being Subset-Family of T st F is Cover of T & F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st ( Y in F & X c< Y ) ) } holds F1 is Cover of T proofend; theorem Th46: :: RCOMP_3:46 for S being 1 -element 1-sorted for s being Point of S for F being Subset-Family of S st F is Cover of S holds {s} in F proofend; definition let T be TopStruct ; let F be Subset-Family of T; attrF is connected means :Def1: :: RCOMP_3:def 1 for X being Subset of T st X in F holds X is connected ; end; :: deftheorem Def1 defines connected RCOMP_3:def_1_:_ for T being TopStruct for F being Subset-Family of T holds ( F is connected iff for X being Subset of T st X in F holds X is connected ); registration let T be TopSpace; cluster non empty open closed connected for Element of K32(K32( the carrier of T)); existence ex b1 being Subset-Family of T st ( not b1 is empty & b1 is open & b1 is closed & b1 is connected ) proofend; end; Lm3: for r, s being real number for F being Subset-Family of (Closed-Interval-TSpace (r,s)) st [.r,s.] in F & r <= s holds ( rng <*[.r,s.]*> c= F & union (rng <*[.r,s.]*>) = [.r,s.] & ( for n being Nat st 1 <= n holds ( ( n <= len <*[.r,s.]*> implies not <*[.r,s.]*> /. n is empty ) & ( n + 1 <= len <*[.r,s.]*> implies ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) ) ) & ( n + 2 <= len <*[.r,s.]*> implies upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) ) ) ) ) proofend; theorem Th47: :: RCOMP_3:47 for L being TopSpace for G, G1 being Subset-Family of L st G is Cover of L & G is finite holds for ALL being set st G1 = G \ { X where X is Subset of L : ( X in G & ex Y being Subset of L st ( Y in G & X c< Y ) ) } & ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G1 ) } holds ALL has_lower_Zorn_property_wrt RelIncl ALL proofend; theorem Th48: :: RCOMP_3:48 for L being TopSpace for G, ALL being set st ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G ) } holds for M being set st M is_minimal_in RelIncl ALL & M in field (RelIncl ALL) holds for A1 being Subset of L st A1 in M holds for A2, A3 being Subset of L holds ( not A2 in M or not A3 in M or not A1 c= A2 \/ A3 or not A1 <> A2 or not A1 <> A3 ) proofend; definition let r, s be real number ; let F be Subset-Family of (Closed-Interval-TSpace (r,s)); assume that B1: F is Cover of (Closed-Interval-TSpace (r,s)) and B2: F is open and B3: F is connected and B4: r <= s ; mode IntervalCover of F -> FinSequence of bool REAL means :Def2: :: RCOMP_3:def 2 ( rng it c= F & union (rng it) = [.r,s.] & ( for n being Nat st 1 <= n holds ( ( n <= len it implies not it /. n is empty ) & ( n + 1 <= len it implies ( lower_bound (it /. n) <= lower_bound (it /. (n + 1)) & upper_bound (it /. n) <= upper_bound (it /. (n + 1)) & lower_bound (it /. (n + 1)) < upper_bound (it /. n) ) ) & ( n + 2 <= len it implies upper_bound (it /. n) <= lower_bound (it /. (n + 2)) ) ) ) & ( [.r,s.] in F implies it = <*[.r,s.]*> ) & ( not [.r,s.] in F implies ( ex p being real number st ( r < p & p <= s & it . 1 = [.r,p.[ ) & ex p being real number st ( r <= p & p < s & it . (len it) = ].p,s.] ) & ( for n being Nat st 1 < n & n < len it holds ex p, q being real number st ( r <= p & p < q & q <= s & it . n = ].p,q.[ ) ) ) ) ); existence ex b1 being FinSequence of bool REAL st ( rng b1 c= F & union (rng b1) = [.r,s.] & ( for n being Nat st 1 <= n holds ( ( n <= len b1 implies not b1 /. n is empty ) & ( n + 1 <= len b1 implies ( lower_bound (b1 /. n) <= lower_bound (b1 /. (n + 1)) & upper_bound (b1 /. n) <= upper_bound (b1 /. (n + 1)) & lower_bound (b1 /. (n + 1)) < upper_bound (b1 /. n) ) ) & ( n + 2 <= len b1 implies upper_bound (b1 /. n) <= lower_bound (b1 /. (n + 2)) ) ) ) & ( [.r,s.] in F implies b1 = <*[.r,s.]*> ) & ( not [.r,s.] in F implies ( ex p being real number st ( r < p & p <= s & b1 . 1 = [.r,p.[ ) & ex p being real number st ( r <= p & p < s & b1 . (len b1) = ].p,s.] ) & ( for n being Nat st 1 < n & n < len b1 holds ex p, q being real number st ( r <= p & p < q & q <= s & b1 . n = ].p,q.[ ) ) ) ) ) proofend; end; :: deftheorem Def2 defines IntervalCover RCOMP_3:def_2_:_ for r, s being real number 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 b4 being FinSequence of bool REAL holds ( b4 is IntervalCover of F iff ( rng b4 c= F & union (rng b4) = [.r,s.] & ( for n being Nat st 1 <= n holds ( ( n <= len b4 implies not b4 /. n is empty ) & ( n + 1 <= len b4 implies ( lower_bound (b4 /. n) <= lower_bound (b4 /. (n + 1)) & upper_bound (b4 /. n) <= upper_bound (b4 /. (n + 1)) & lower_bound (b4 /. (n + 1)) < upper_bound (b4 /. n) ) ) & ( n + 2 <= len b4 implies upper_bound (b4 /. n) <= lower_bound (b4 /. (n + 2)) ) ) ) & ( [.r,s.] in F implies b4 = <*[.r,s.]*> ) & ( not [.r,s.] in F implies ( ex p being real number st ( r < p & p <= s & b4 . 1 = [.r,p.[ ) & ex p being real number st ( r <= p & p < s & b4 . (len b4) = ].p,s.] ) & ( for n being Nat st 1 < n & n < len b4 holds ex p, q being real number st ( r <= p & p < q & q <= s & b4 . n = ].p,q.[ ) ) ) ) ) ); theorem :: RCOMP_3:49 for r, s being real number 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 & [.r,s.] in F holds <*[.r,s.]*> is IntervalCover of F proofend; theorem Th50: :: RCOMP_3:50 for r being real number for F being Subset-Family of (Closed-Interval-TSpace (r,r)) for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,r)) & F is open & F is connected holds C = <*[.r,r.]*> proofend; theorem Th51: :: RCOMP_3:51 for r, s being real number 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 1 <= len C proofend; theorem Th52: :: RCOMP_3:52 for r, s being real number 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 & len C = 1 holds C = <*[.r,s.]*> proofend; theorem :: RCOMP_3:53 for r, s being real number for n, m being Nat 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 & n in dom C & m in dom C & n < m holds lower_bound (C /. n) <= lower_bound (C /. m) proofend; theorem :: RCOMP_3:54 for r, s being real number for n, m being Nat 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 & n in dom C & m in dom C & n < m holds upper_bound (C /. n) <= upper_bound (C /. m) proofend; theorem Th55: :: RCOMP_3:55 for r, s being real number for n being Nat 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 & 1 <= n & n + 1 <= len C holds not ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ is empty proofend; theorem :: RCOMP_3:56 for r, s being real number 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 lower_bound (C /. 1) = r proofend; theorem Th57: :: RCOMP_3:57 for r, s being real number 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 r in C /. 1 proofend; theorem :: RCOMP_3:58 for r, s being real number 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 upper_bound (C /. (len C)) = s proofend; theorem Th59: :: RCOMP_3:59 for r, s being real number 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 s in C /. (len C) proofend; definition let r, s be real number ; let F be Subset-Family of (Closed-Interval-TSpace (r,s)); let C be IntervalCover of F; assume B1: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s ) ; mode IntervalCoverPts of C -> FinSequence of REAL means :Def3: :: RCOMP_3:def 3 ( len it = (len C) + 1 & it . 1 = r & it . (len it) = s & ( for n being Nat st 1 <= n & n + 1 < len it holds it . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) ); existence ex b1 being FinSequence of REAL st ( len b1 = (len C) + 1 & b1 . 1 = r & b1 . (len b1) = s & ( for n being Nat st 1 <= n & n + 1 < len b1 holds b1 . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) ) proofend; end; :: deftheorem Def3 defines IntervalCoverPts RCOMP_3:def_3_:_ for r, s being real number 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 b5 being FinSequence of REAL holds ( b5 is IntervalCoverPts of C iff ( len b5 = (len C) + 1 & b5 . 1 = r & b5 . (len b5) = s & ( for n being Nat st 1 <= n & n + 1 < len b5 holds b5 . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) ) ); theorem Th60: :: RCOMP_3:60 for r, s being real number 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 holds 2 <= len G proofend; theorem Th61: :: RCOMP_3:61 for r, s being real number 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 & len C = 1 holds G = <*r,s*> proofend; theorem Th62: :: RCOMP_3:62 for r, s being real number 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 + 1 < len G holds G . (n + 1) < upper_bound (C /. n) proofend; theorem Th63: :: RCOMP_3:63 for r, s being real number 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 lower_bound (C /. n) < G . n proofend; theorem Th64: :: RCOMP_3:64 for r, s being real number 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)) proofend; theorem Th65: :: RCOMP_3:65 for r, s being real number 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 holds G is increasing proofend; theorem :: RCOMP_3:66 for r, s being real number 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 G holds [.(G . n),(G . (n + 1)).] c= C . n proofend;