:: Properties of Connected Subsets of the Real Line
:: by Artur Korni{\l}owicz
::
:: Received February 22, 2005
:: Copyright (c) 2005-2011 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 SubSpace of RealSpace ;
coherence
for b₁ being SubSpace of RealSpace holds b₁ 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;

begin

registration

let r be real number ;
let s be ext-real number ;
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 number ;
cluster [.r,s.[ -> bounded ;
coherence
[.r,s.[ is bounded

proof end;

cluster ].r,s.] -> bounded ;
coherence
].r,s.] is bounded

proof end;

cluster ].r,s.[ -> bounded ;
coherence
].r,s.[ is bounded

proof end;

end;

registration

cluster non empty complex-membered ext-real-membered real-membered open bounded interval Element of K10(REAL);
existence
ex b₁ being Subset of REAL st
( b₁ is open & b₁ is bounded & b₁ is interval & not b₁ is empty )

proof end;

end;

theorem Th4: :: RCOMP_3:4

for r, s being real number st r < s holds
lower_bound [.r,s.[ = r

proof end;

theorem Th5: :: RCOMP_3:5

for r, s being real number st r < s holds
upper_bound [.r,s.[ = s

proof end;

theorem Th6: :: RCOMP_3:6

for r, s being real number st r < s holds
lower_bound ].r,s.] = r

proof end;

theorem Th7: :: RCOMP_3:7

for r, s being real number st r < s holds
upper_bound ].r,s.] = s

proof end;

begin

theorem :: RCOMP_3:8

canceled;

theorem :: RCOMP_3:9

canceled;

theorem :: RCOMP_3:10

canceled;

theorem :: RCOMP_3:11

canceled;

theorem :: RCOMP_3:12

canceled;

theorem :: RCOMP_3:13

canceled;

theorem :: RCOMP_3:14

canceled;

theorem :: RCOMP_3:15

canceled;

theorem :: RCOMP_3:16

canceled;

theorem :: RCOMP_3:17

canceled;

theorem :: RCOMP_3:18

canceled;

theorem :: RCOMP_3:19

canceled;

theorem Th20: :: RCOMP_3:20

for a, b being real number st a <= b holds
[.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b}

proof end;

Lm1: now

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:17;
then a - 1 in left_open_halfline a by XXREAL_1:233;
then b - 1 < (a - 1) - 0 by A2, XREAL_1:17;
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:17; :: thesis: verum

end;

Lm2: now

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;
A3: a + 0 < a + 1 by XREAL_1:8;
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:9;
then a < b + 1 by A3, 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:8; :: 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 )

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 Th21: :: RCOMP_3:21

for a being real number holds upper_bound (left_closed_halfline a) = a

proof end;

theorem Th22: :: RCOMP_3:22

for a being real number holds upper_bound (left_open_halfline a) = a

proof end;

theorem Th23: :: RCOMP_3:23

for a being real number holds lower_bound (right_closed_halfline a) = a

proof end;

theorem Th24: :: RCOMP_3:24

for a being real number holds lower_bound (right_open_halfline a) = a

proof end;

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 Th25: :: RCOMP_3:25

for X being 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 Th26: :: RCOMP_3:26

for X being bounded Subset of REAL st not lower_bound X in X holds
X c= ].(lower_bound X),(upper_bound X).]

proof end;

theorem Th27: :: RCOMP_3:27

for X being 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 Th28: :: RCOMP_3:28

for X being bounded Subset of REAL st not upper_bound X in X holds
X c= [.(lower_bound X),(upper_bound X).[

proof end;

theorem Th29: :: RCOMP_3:29

for X being 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 Th30: :: RCOMP_3:30

for X being 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 Th31: :: RCOMP_3:31

for X being non empty 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 Th32: :: RCOMP_3:32

for X being Subset of REAL st X is bounded_above holds
X c= left_closed_halfline (upper_bound X)

proof end;

theorem Th33: :: RCOMP_3:33

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 Th34: :: RCOMP_3:34

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 Th35: :: RCOMP_3:35

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 Th36: :: RCOMP_3:36

for X being Subset of REAL st X is bounded_below holds
X c= right_closed_halfline (lower_bound X)

proof end;

theorem Th37: :: RCOMP_3:37

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 Th38: :: RCOMP_3:38

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 Th39: :: RCOMP_3:39

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 Th40: :: RCOMP_3:40

for X being interval Subset of REAL st not X is bounded_above & not X is bounded_below holds
X = REAL

proof end;

theorem Th41: :: RCOMP_3:41

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.[ ) )

proof end;

theorem Th42: :: RCOMP_3:42

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 )

proof end;

theorem Th43: :: RCOMP_3:43

for X, Y being non empty 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 bounded interval Element of K10(REAL);
existence
ex b₁ being Subset of REAL st
( b₁ is open & b₁ is closed & b₁ is interval & not b₁ is empty & not b₁ is bounded )

proof end;

end;

begin

theorem Th44: :: RCOMP_3:44

for a, b being real number
for X being Subset of R^1 st a <= b & X = [.a,b.] holds
Fr X = {a,b}

proof end;

theorem :: RCOMP_3:45

for a, b being real number
for X being Subset of R^1 st a < b & X = ].a,b.[ holds
Fr X = {a,b}

proof end;

theorem Th46: :: RCOMP_3:46

for a, b being real number
for X being Subset of R^1 st a < b & X = [.a,b.[ holds
Fr X = {a,b}

proof end;

theorem Th47: :: RCOMP_3:47

for a, b being real number
for X being Subset of R^1 st a < b & X = ].a,b.] holds
Fr X = {a,b}

proof end;

theorem :: RCOMP_3:48

for a, b being real number
for X being Subset of R^1 st X = [.a,b.] holds
Int X = ].a,b.[

proof end;

theorem :: RCOMP_3:49

for a, b being real number
for X being Subset of R^1 st X = ].a,b.[ holds
Int X = ].a,b.[

proof end;

theorem Th50: :: RCOMP_3:50

for a, b being real number
for X being Subset of R^1 st X = [.a,b.[ holds
Int X = ].a,b.[

proof end;

theorem Th51: :: RCOMP_3:51

for a, b being real number
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

proof end;

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 Element of K10( the carrier of R^1);
coherence
for b₁ being Subset of R^1 st b₁ is connected holds
b₁ is interval

proof end;

cluster interval -> connected Element of K10( the carrier of R^1);
coherence
for b₁ being Subset of R^1 st b₁ is interval holds
b₁ is connected

proof end;

end;

begin

registration

let r be real number ;
cluster Closed-Interval-TSpace (r,r) -> trivial ;
coherence
Closed-Interval-TSpace (r,r) is trivial

proof end;

end;

theorem :: RCOMP_3:52

canceled;

theorem :: RCOMP_3:53

for r, s being real number st r <= s holds
for A being Subset of (Closed-Interval-TSpace (r,s)) holds A is bounded Subset of REAL

proof end;

theorem Th54: :: RCOMP_3:54

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.[

proof end;

theorem Th55: :: RCOMP_3:55

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.[

proof end;

theorem Th56: :: RCOMP_3:56

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 )

proof end;

registration

let T be TopSpace;
cluster open closed connected Element of K10( the carrier of T);
existence
ex b₁ being Subset of T st
( b₁ is open & b₁ is closed & b₁ is connected )

proof end;

end;

registration

let T be non empty connected TopSpace;
cluster non empty open closed connected Element of K10( the carrier of T);
existence
ex b₁ being Subset of T st
( not b₁ is empty & b₁ is open & b₁ is closed & b₁ is connected )

proof end;

end;

theorem Th57: :: RCOMP_3:57

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.[ ) )

proof end;

begin

deffunc H₁( set ) -> set = $1;

defpred S₁[ set , set ] means $1 c= $2;

theorem :: RCOMP_3:58

canceled;

theorem Th59: :: RCOMP_3:59

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 Th60: :: RCOMP_3:60

for S being non empty trivial 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 :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 Element of K10(K10( the carrier of T));
existence
ex b₁ being Subset-Family of T st
( not b₁ is empty & b₁ is open & b₁ is closed & b₁ is connected )

proof end;

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 natural number 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 Th61: :: RCOMP_3:61

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 Th62: :: RCOMP_3:62

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;

definition

let r, s be real number ;
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 natural number 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 natural number 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 b₁ being FinSequence of bool REAL st
( rng b₁ c= F & union (rng b₁) = [.r,s.] & ( for n being natural number 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 number st
( r < p & p <= s & b₁ . 1 = [.r,p.[ ) & ex p being real number st
( r <= p & p < s & b₁ . (len b₁) = ].p,s.] ) & ( for n being natural number st 1 < n & n < len b₁ holds
ex p, q being real number st
( r <= p & p < q & q <= s & b₁ . n = ].p,q.[ ) ) ) ) )

proof end;

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 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 natural number 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 number st
( r < p & p <= s & b₄ . 1 = [.r,p.[ ) & ex p being real number st
( r <= p & p < s & b₄ . (len b₄) = ].p,s.] ) & ( for n being natural number st 1 < n & n < len b₄ holds
ex p, q being real number st
( r <= p & p < q & q <= s & b₄ . n = ].p,q.[ ) ) ) ) ) );

theorem :: RCOMP_3:63

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

proof end;

theorem Th64: :: RCOMP_3:64

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.]*>

proof end;

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 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 Th66: :: RCOMP_3:66

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.]*>

proof end;

theorem :: RCOMP_3:67

for r, s being real number
for n, m being natural 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 & n in dom C & m in dom C & n < m holds
lower_bound (C /. n) <= lower_bound (C /. m)

proof end;

theorem :: RCOMP_3:68

for r, s being real number
for n, m being natural 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 & n in dom C & m in dom C & n < m holds
upper_bound (C /. n) <= upper_bound (C /. m)

proof end;

theorem Th69: :: RCOMP_3:69

for r, s being real number
for n being natural 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 & 1 <= n & n + 1 <= len C holds
not ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ is empty

proof end;

theorem :: RCOMP_3:70

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

proof end;

theorem Th71: :: RCOMP_3:71

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

proof end;

theorem :: RCOMP_3:72

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

proof end;

theorem Th73: :: RCOMP_3:73

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)

proof end;

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 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 natural number st 1 <= n & n + 1 < len it holds
it . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) );
existence
ex b₁ being FinSequence of REAL st
( len b₁ = (len C) + 1 & b₁ . 1 = r & b₁ . (len b₁) = s & ( for n being natural number st 1 <= n & n + 1 < len b₁ holds
b₁ . (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 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 b₅ being FinSequence of REAL holds
( b₅ is IntervalCoverPts of C iff ( len b₅ = (len C) + 1 & b₅ . 1 = r & b₅ . (len b₅) = s & ( for n being natural number st 1 <= n & n + 1 < len b₅ holds
b₅ . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) ) );

theorem Th74: :: RCOMP_3:74

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

proof end;

theorem Th75: :: RCOMP_3:75

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*>

proof end;

theorem Th76: :: RCOMP_3:76

for r, s being real number
for n being natural 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 & 1 <= n & n + 1 < len G holds
G . (n + 1) < upper_bound (C /. n)

proof end;

theorem Th77: :: RCOMP_3:77

for r, s being real number
for n being natural 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 & 1 < n & n <= len C holds
lower_bound (C /. n) < G . n

proof end;

theorem Th78: :: RCOMP_3:78

for r, s being real number
for n being natural 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 & 1 <= n & n < len C holds
G . n <= lower_bound (C /. (n + 1))

proof end;

theorem Th79: :: RCOMP_3:79

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

proof end;

theorem :: RCOMP_3:80

for r, s being real number
for n being natural 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 & 1 <= n & n < len G holds
[.(G . n),(G . (n + 1)).] c= C . n

proof end;