:: Properties of Connected Subsets of the Real Line
:: by Artur Korni{\l}owicz
::
:: Received February 22, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users


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
proof end;
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
proof end;

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
proof end;

theorem Th3: :: RCOMP_3:3
for X, Y being Subset of REAL holds Cl (X \/ Y) = (Cl X) \/ (Cl Y)
proof end;

registration
let r be Real;
let s be ExtReal;
cluster [.r,s.[ -> bounded_below ;
coherence
[.r,s.[ is bounded_below
proof end;
cluster ].s,r.] -> bounded_above ;
coherence
].s,r.] is bounded_above
proof end;
end;

registration
let r, s be Real;
cluster [.r,s.[ -> real-bounded ;
coherence
[.r,s.[ is real-bounded
proof end;
cluster ].r,s.] -> real-bounded ;
coherence
].r,s.] is real-bounded
proof end;
cluster ].r,s.[ -> real-bounded ;
coherence
].r,s.[ is real-bounded
proof end;
end;

registration
cluster non empty complex-membered ext-real-membered real-membered open real-bounded interval for Element of K34(REAL);
existence
ex b1 being Subset of REAL st
( b1 is open & b1 is real-bounded & b1 is interval & not b1 is empty )
proof end;
end;

theorem Th4: :: RCOMP_3:4
for r, s being Real st r < s holds
lower_bound [.r,s.[ = r
proof end;

theorem Th5: :: RCOMP_3:5
for r, s being Real st r < s holds
upper_bound [.r,s.[ = s
proof end;

theorem Th6: :: RCOMP_3:6
for r, s being Real st r < s holds
lower_bound ].r,s.] = r
proof end;

theorem Th7: :: RCOMP_3:7
for r, s being Real st r < s holds
upper_bound ].r,s.] = s
proof end;

theorem Th8: :: RCOMP_3:8
for a, b being Real st a <= b holds
[.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b}
proof end;

Lm1: now :: thesis: for a being Real holds not left_open_halfline a is bounded_below
let a be Real; :: thesis: not left_open_halfline a is bounded_below
assume left_open_halfline a is bounded_below ; :: thesis: contradiction
then consider b being Real such that
A1: b is LowerBound of left_open_halfline a ;
A2: for r being Real 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 holds not right_open_halfline a is bounded_above
let a be Real; :: thesis: not right_open_halfline a is bounded_above
assume right_open_halfline a is bounded_above ; :: thesis: contradiction
then consider b being Real such that
A1: b is UpperBound of right_open_halfline a ;
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;
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 )
proof end;
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 )
proof end;
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 )
proof end;
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 )
proof end;
end;

theorem Th9: :: RCOMP_3:9
for a being Real holds upper_bound (left_closed_halfline a) = a
proof end;

theorem Th10: :: RCOMP_3:10
for a being Real holds upper_bound (left_open_halfline a) = a
proof end;

theorem Th11: :: RCOMP_3:11
for a being Real holds lower_bound (right_closed_halfline a) = a
proof end;

theorem Th12: :: RCOMP_3:12
for a being Real holds lower_bound (right_open_halfline a) = a
proof end;

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).]
proof end;

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).]
proof end;

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).]
proof end;

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).[
proof end;

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).[
proof end;

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).[
proof end;

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).[
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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
proof end;

theorem Th29: :: RCOMP_3:29
for X being interval Subset of REAL holds
( X is empty or X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )
proof end;

theorem Th30: :: RCOMP_3:30
for r being Real
for X being non empty interval Subset of REAL holds
( r in X or r <= lower_bound X or upper_bound X <= r )
proof end;

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
proof end;

registration
cluster non empty complex-membered ext-real-membered real-membered closed open non real-bounded interval for Element of K34(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 )
proof end;
end;

theorem Th32: :: RCOMP_3:32
for a, b being Real
for X being Subset of R^1 st a <= b & X = [.a,b.] holds
Fr X = {a,b}
proof end;

theorem :: RCOMP_3:33
for a, b being Real
for X being Subset of R^1 st a < b & X = ].a,b.[ holds
Fr X = {a,b}
proof end;

theorem Th34: :: RCOMP_3:34
for a, b being Real
for X being Subset of R^1 st a < b & X = [.a,b.[ holds
Fr X = {a,b}
proof end;

theorem Th35: :: RCOMP_3:35
for a, b being Real
for X being Subset of R^1 st a < b & X = ].a,b.] holds
Fr X = {a,b}
proof end;

theorem :: RCOMP_3:36
for a, b being Real
for X being Subset of R^1 st X = [.a,b.] holds
Int X = ].a,b.[
proof end;

theorem :: RCOMP_3:37
for a, b being Real
for X being Subset of R^1 st X = ].a,b.[ holds
Int X = ].a,b.[
proof end;

theorem Th38: :: RCOMP_3:38
for a, b being Real
for X being Subset of R^1 st X = [.a,b.[ holds
Int X = ].a,b.[
proof end;

theorem Th39: :: RCOMP_3:39
for a, b being Real
for X being Subset of R^1 st X = ].a,b.] holds
Int X = ].a,b.[
proof end;

registration
let T be real-membered TopStruct ;
let X be interval Subset of T;
cluster T | X -> interval ;
coherence
T | X is interval by PRE_TOPC:def 5;
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 K34( the carrier of R^1);
coherence
for b1 being Subset of R^1 st b1 is connected holds
b1 is interval by BORSUK_5:77;
cluster interval -> connected for Element of K34( the carrier of R^1);
coherence
for b1 being Subset of R^1 st b1 is interval holds
b1 is connected
proof end;
end;

registration
let r be Real;
cluster Closed-Interval-TSpace (r,r) -> 1 -element ;
coherence
Closed-Interval-TSpace (r,r) is 1 -element
proof end;
end;

theorem :: RCOMP_3:40
for r, s being Real st r <= s holds
for A being Subset of (Closed-Interval-TSpace (r,s)) holds A is real-bounded Subset of REAL
proof end;

theorem Th41: :: RCOMP_3:41
for a, b, r, s being Real 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.[
proof end;

theorem Th42: :: RCOMP_3:42
for a, b, r, s being Real 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.[
proof end;

theorem Th43: :: RCOMP_3:43
for r, s being Real
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 )
proof end;

registration
let T be TopSpace;
cluster open closed connected for Element of K34( the carrier of T);
existence
ex b1 being Subset of T st
( b1 is open & b1 is closed & b1 is connected )
proof end;
end;

registration
let T be non empty connected TopSpace;
cluster non empty open closed connected for Element of K34( 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 )
proof end;
end;

theorem Th44: :: RCOMP_3:44
for r, s being Real 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 st
( r < a & a <= s & X = [.r,a.[ ) or ex a being Real st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being Real st
( r <= a & a < b & b <= s & X = ].a,b.[ ) )
proof end;

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
proof end;

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
proof end;

definition
let T be TopStruct ;
let F be Subset-Family of T;
attr F is connected means :: RCOMP_3:def 1
 for X being Subset of T st X in F holds
X is connected ;
end;

:: deftheorem 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 K34(K34( 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 )
proof end;
end;

Lm3: for r, s being Real
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)) ) ) ) )
proof end;

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
proof end;

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 )
proof end;

registration
let X be Subset-Family of REAL;
cluster -> real-membered for Element of X;
coherence
for b1 being Element of X holds b1 is real-membered
proof end;
end;

definition
let r, s be Real;
let F be Subset-Family of (Closed-Interval-TSpace (r,s));
assume that
A1: F is Cover of (Closed-Interval-TSpace (r,s)) and
A2: F is open and
A3: F is connected and
A4: 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 st
( r < p & p <= s & it . 1 = [.r,p.[ ) & ex p being Real 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 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 st
( r < p & p <= s & b1 . 1 = [.r,p.[ ) & ex p being Real 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 st
( r <= p & p < q & q <= s & b1 . n = ].p,q.[ ) ) ) ) )
proof end;
end;

:: 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 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 st
( r < p & p <= s & b4 . 1 = [.r,p.[ ) & ex p being Real 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 st
( r <= p & p < q & q <= s & b4 . n = ].p,q.[ ) ) ) ) ) );

theorem :: RCOMP_3:49
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 & [.r,s.] in F holds
<*[.r,s.]*> is IntervalCover of F
proof end;

theorem Th50: :: RCOMP_3:50
for r being Real
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.]*>
proof end;

theorem Th51: :: RCOMP_3:51
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
1 <= len C
proof end;

theorem Th52: :: RCOMP_3:52
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 & len C = 1 holds
C = <*[.r,s.]*>
proof end;

theorem :: RCOMP_3:53
for r, s being Real
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)
proof end;

theorem :: RCOMP_3:54
for r, s being Real
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)
proof end;

theorem Th55: :: RCOMP_3:55
for r, s being Real
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
proof end;

theorem :: RCOMP_3:56
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
lower_bound (C /. 1) = r
proof end;

theorem Th57: :: RCOMP_3:57
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
r in C /. 1
proof end;

theorem :: RCOMP_3:58
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
upper_bound (C /. (len C)) = s
proof end;

theorem Th59: :: RCOMP_3:59
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
s in C /. (len C)
proof end;

definition
let r, s be Real;
let F be Subset-Family of (Closed-Interval-TSpace (r,s));
let C be IntervalCover of F;
assume A1: ( 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)).[ ) )
proof end;
end;

:: 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 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
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
proof end;

theorem Th61: :: RCOMP_3:61
for r, s being Real
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*>
proof end;

theorem Th62: :: RCOMP_3:62
for r, s being Real
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)
proof end;

theorem Th63: :: RCOMP_3:63
for r, s being Real
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
proof end;

theorem Th64: :: RCOMP_3:64
for r, s being Real
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))
proof end;

theorem Th65: :: RCOMP_3:65
for r, s being Real
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
proof end;

theorem :: RCOMP_3:66
for r, s being Real
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
proof end;