:: RCOMP_3 semantic presentation

Lemma1: REAL = [#] REAL
by SUBSET_1:def 4;

registration

let c₁ be non empty set ;
cluster [#] a₁ -> non empty ;
coherence by SUBSET_1:def 4;

end;

registration

cluster -> real-membered SubSpace of RealSpace ;
coherence

proof end;

end;

registration

let c₁ be real-membered 1-sorted ;
cluster the carrier of a₁ -> real-membered ;
coherence by BORSUK_6:def 1;

end;

registration

cluster non empty finite real-membered bounded_above bounded_below set ;
existence

proof end;

end;

theorem Th1: :: RCOMP_3:1

for b₁ being non empty real-membered bounded_below set
for b₂ being closed Subset of REAL st b₁ c= b₂ holds
inf b₁ in b₂

proof end;

theorem Th2: :: RCOMP_3:2

for b₁ being non empty real-membered bounded_above set
for b₂ being closed Subset of REAL st b₁ c= b₂ holds
sup b₁ in b₂

proof end;

theorem Th3: :: RCOMP_3:3

for b₁, b₂ being Subset of REAL holds Cl (b₁ \/ b₂) = (Cl b₁) \/ (Cl b₂)

proof end;

registration

let c₁, c₂ be real number ;
cluster [.a₁,a₂.[ -> bounded ;
coherence

proof end;

cluster ].a₁,a₂.] -> bounded ;
coherence

proof end;

cluster ].a₁,a₂.[ -> bounded ;
coherence

proof end;

end;

registration

let c₁, c₂ be real number ;
cluster [.a₁,a₂.] -> connected ;
coherence

proof end;

cluster [.a₁,a₂.[ -> bounded connected ;
coherence

proof end;

cluster ].a₁,a₂.] -> bounded connected ;
coherence

proof end;

cluster ].a₁,a₂.[ -> bounded connected ;
coherence

proof end;

end;

registration

cluster non empty bounded open connected Element of K10(REAL );
existence

proof end;

end;

theorem Th4: :: RCOMP_3:4

for b₁, b₂ being real number st b₁ < b₂ holds
inf [.b₁,b₂.[ = b₁

proof end;

theorem Th5: :: RCOMP_3:5

for b₁, b₂ being real number st b₁ < b₂ holds
sup [.b₁,b₂.[ = b₂

proof end;

theorem Th6: :: RCOMP_3:6

for b₁, b₂ being real number st b₁ < b₂ holds
inf ].b₁,b₂.] = b₁

proof end;

theorem Th7: :: RCOMP_3:7

for b₁, b₂ being real number st b₁ < b₂ holds
sup ].b₁,b₂.] = b₂

proof end;

theorem Th8: :: RCOMP_3:8

for b₁, b₂, b₃, b₄ being real number st ( b₁ <= b₂ or b₃ <= b₄ ) & [.b₁,b₂.] = [.b₃,b₄.] holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th9: :: RCOMP_3:9

for b₁, b₂, b₃, b₄ being real number st ( b₁ < b₂ or b₃ < b₄ ) & ].b₁,b₂.[ = ].b₃,b₄.[ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th10: :: RCOMP_3:10

for b₁, b₂, b₃, b₄ being real number st ( b₁ < b₂ or b₃ < b₄ ) & ].b₁,b₂.] = ].b₃,b₄.] holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th11: :: RCOMP_3:11

for b₁, b₂, b₃, b₄ being real number st ( b₁ < b₂ or b₃ < b₄ ) & [.b₁,b₂.[ = [.b₃,b₄.[ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th12: :: RCOMP_3:12

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & [.b₁,b₂.[ c= [.b₃,b₄.] holds
( b₃ <= b₁ & b₂ <= b₄ )

proof end;

theorem Th13: :: RCOMP_3:13

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & [.b₁,b₂.[ c= [.b₃,b₄.[ holds
( b₃ <= b₁ & b₂ <= b₄ )

proof end;

theorem Th14: :: RCOMP_3:14

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & ].b₁,b₂.] c= [.b₃,b₄.] holds
( b₃ <= b₁ & b₂ <= b₄ )

proof end;

theorem Th15: :: RCOMP_3:15

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & ].b₁,b₂.] c= ].b₃,b₄.] holds
( b₃ <= b₁ & b₂ <= b₄ )

proof end;

theorem Th16: :: RCOMP_3:16

for b₁, b₂ being real number holds [.b₁,b₂.] ` = (left_open_halfline b₁) \/ (right_open_halfline b₂)

proof end;

theorem Th17: :: RCOMP_3:17

for b₁, b₂ being real number holds ].b₁,b₂.[ ` = (left_closed_halfline b₁) \/ (right_closed_halfline b₂)

proof end;

theorem Th18: :: RCOMP_3:18

for b₁, b₂ being real number holds [.b₁,b₂.[ ` = (left_open_halfline b₁) \/ (right_closed_halfline b₂)

proof end;

theorem Th19: :: RCOMP_3:19

for b₁, b₂ being real number holds ].b₁,b₂.] ` = (left_closed_halfline b₁) \/ (right_open_halfline b₂)

proof end;

theorem Th20: :: RCOMP_3:20

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

proof end;

E16: now

let c₁ be real number ;
assume left_open_halfline c₁ is bounded_below ;
then consider c₂ being real number such that
E17: for b₁ being real number st b₁ in left_open_halfline c₁ holds
c₂ <= b₁ by SEQ_4:def 2;
E18: c₁ - 1 < c₁ - 0 by XREAL_1:17;
then c₁ - 1 in left_open_halfline c₁ by BORSUK_5:17;
then c₂ <= c₁ - 1 by E17;
then c₂ - 1 < (c₁ - 1) - 0 by XREAL_1:17;
then c₂ - 1 < c₁ by E18, XREAL_1:2;
then c₂ - 1 in left_open_halfline c₁ by BORSUK_5:17;
then c₂ - 0 <= c₂ - 1 by E17;
hence contradiction by XREAL_1:17;

end;

E17: now

let c₁ be real number ;
assume right_open_halfline c₁ is bounded_above ;
then consider c₂ being real number such that
E18: for b₁ being real number st b₁ in right_open_halfline c₁ holds
b₁ <= c₂ by SEQ_4:def 1;
E19: c₁ + 0 < c₁ + 1 by XREAL_1:8;
then c₁ + 1 in right_open_halfline c₁ by BORSUK_5:14;
then c₁ + 1 <= c₂ by E18;
then (c₁ + 1) + 0 <= c₂ + 1 by XREAL_1:9;
then c₁ < c₂ + 1 by E19, XREAL_1:2;
then c₂ + 1 in right_open_halfline c₁ by BORSUK_5:14;
then c₂ + 1 <= c₂ + 0 by E18;
hence contradiction by XREAL_1:8;

end;

registration

let c₁ be real number ;
cluster left_closed_halfline a₁ -> bounded_above non bounded_below connected ;
coherence

proof end;

cluster left_open_halfline a₁ -> bounded_above non bounded_below connected ;
coherence

proof end;

cluster right_closed_halfline a₁ -> non bounded_above bounded_below connected ;
coherence

proof end;

cluster right_open_halfline a₁ -> non bounded_above bounded_below connected ;
coherence

proof end;

end;

theorem Th21: :: RCOMP_3:21

for b₁ being real number holds sup (left_closed_halfline b₁) = b₁

proof end;

theorem Th22: :: RCOMP_3:22

for b₁ being real number holds sup (left_open_halfline b₁) = b₁

proof end;

theorem Th23: :: RCOMP_3:23

for b₁ being real number holds inf (right_closed_halfline b₁) = b₁

proof end;

theorem Th24: :: RCOMP_3:24

for b₁ being real number holds inf (right_open_halfline b₁) = b₁

proof end;

registration

cluster [#] REAL -> non empty non bounded_above non bounded_below connected ;
coherence

proof end;

end;

theorem Th25: :: RCOMP_3:25

for b₁ being bounded connected Subset of REAL st inf b₁ in b₁ & sup b₁ in b₁ holds
b₁ = [.(inf b₁),(sup b₁).]

proof end;

theorem Th26: :: RCOMP_3:26

for b₁ being bounded Subset of REAL st not inf b₁ in b₁ holds
b₁ c= ].(inf b₁),(sup b₁).]

proof end;

theorem Th27: :: RCOMP_3:27

for b₁ being bounded connected Subset of REAL st not inf b₁ in b₁ & sup b₁ in b₁ holds
b₁ = ].(inf b₁),(sup b₁).]

proof end;

theorem Th28: :: RCOMP_3:28

for b₁ being bounded Subset of REAL st not sup b₁ in b₁ holds
b₁ c= [.(inf b₁),(sup b₁).[

proof end;

theorem Th29: :: RCOMP_3:29

for b₁ being bounded connected Subset of REAL st inf b₁ in b₁ & not sup b₁ in b₁ holds
b₁ = [.(inf b₁),(sup b₁).[

proof end;

theorem Th30: :: RCOMP_3:30

for b₁ being bounded Subset of REAL st not inf b₁ in b₁ & not sup b₁ in b₁ holds
b₁ c= ].(inf b₁),(sup b₁).[

proof end;

theorem Th31: :: RCOMP_3:31

for b₁ being non empty bounded connected Subset of REAL st not inf b₁ in b₁ & not sup b₁ in b₁ holds
b₁ = ].(inf b₁),(sup b₁).[

proof end;

theorem Th32: :: RCOMP_3:32

for b₁ being Subset of REAL st b₁ is bounded_above holds
b₁ c= left_closed_halfline (sup b₁)

proof end;

theorem Th33: :: RCOMP_3:33

for b₁ being connected Subset of REAL st not b₁ is bounded_below & b₁ is bounded_above & sup b₁ in b₁ holds
b₁ = left_closed_halfline (sup b₁)

proof end;

theorem Th34: :: RCOMP_3:34

for b₁ being Subset of REAL st b₁ is bounded_above & not sup b₁ in b₁ holds
b₁ c= left_open_halfline (sup b₁)

proof end;

theorem Th35: :: RCOMP_3:35

for b₁ being non empty connected Subset of REAL st not b₁ is bounded_below & b₁ is bounded_above & not sup b₁ in b₁ holds
b₁ = left_open_halfline (sup b₁)

proof end;

theorem Th36: :: RCOMP_3:36

for b₁ being Subset of REAL st b₁ is bounded_below holds
b₁ c= right_closed_halfline (inf b₁)

proof end;

theorem Th37: :: RCOMP_3:37

for b₁ being connected Subset of REAL st b₁ is bounded_below & not b₁ is bounded_above & inf b₁ in b₁ holds
b₁ = right_closed_halfline (inf b₁)

proof end;

theorem Th38: :: RCOMP_3:38

for b₁ being Subset of REAL st b₁ is bounded_below & not inf b₁ in b₁ holds
b₁ c= right_open_halfline (inf b₁)

proof end;

theorem Th39: :: RCOMP_3:39

for b₁ being non empty connected Subset of REAL st b₁ is bounded_below & not b₁ is bounded_above & not inf b₁ in b₁ holds
b₁ = right_open_halfline (inf b₁)

proof end;

theorem Th40: :: RCOMP_3:40

for b₁ being connected Subset of REAL st not b₁ is bounded_above & not b₁ is bounded_below holds
b₁ = REAL

proof end;

theorem Th41: :: RCOMP_3:41

for b₁ being connected Subset of REAL holds
( b₁ is empty or b₁ = REAL or ex b₂ being real number st b₁ = left_closed_halfline b₂ or ex b₂ being real number st b₁ = left_open_halfline b₂ or ex b₂ being real number st b₁ = right_closed_halfline b₂ or ex b₂ being real number st b₁ = right_open_halfline b₂ or ex b₂, b₃ being real number st
( b₂ <= b₃ & b₁ = [.b₂,b₃.] ) or ex b₂, b₃ being real number st
( b₂ < b₃ & b₁ = [.b₂,b₃.[ ) or ex b₂, b₃ being real number st
( b₂ < b₃ & b₁ = ].b₂,b₃.] ) or ex b₂, b₃ being real number st
( b₂ < b₃ & b₁ = ].b₂,b₃.[ ) )

proof end;

theorem Th42: :: RCOMP_3:42

for b₁ being real number
for b₂ being non empty connected Subset of REAL holds
( b₁ in b₂ or b₁ <= inf b₂ or sup b₂ <= b₁ )

proof end;

theorem Th43: :: RCOMP_3:43

for b₁, b₂ being non empty bounded connected Subset of REAL st inf b₁ <= inf b₂ & sup b₂ <= sup b₁ & ( inf b₁ = inf b₂ & inf b₂ in b₂ implies inf b₁ in b₁ ) & ( sup b₁ = sup b₂ & sup b₂ in b₂ implies sup b₁ in b₁ ) holds
b₂ c= b₁

proof end;

registration

cluster non empty non bounded closed open connected Element of K10(REAL );
existence

proof end;

end;

theorem Th44: :: RCOMP_3:44

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

proof end;

theorem Th45: :: RCOMP_3:45

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

proof end;

theorem Th46: :: RCOMP_3:46

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

proof end;

theorem Th47: :: RCOMP_3:47

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

proof end;

theorem Th48: :: RCOMP_3:48

for b₁, b₂ being real number
for b₃ being Subset of R^1 st b₃ = [.b₁,b₂.] holds
Int b₃ = ].b₁,b₂.[

proof end;

theorem Th49: :: RCOMP_3:49

for b₁, b₂ being real number
for b₃ being Subset of R^1 st b₃ = ].b₁,b₂.[ holds
Int b₃ = ].b₁,b₂.[

proof end;

theorem Th50: :: RCOMP_3:50

for b₁, b₂ being real number
for b₃ being Subset of R^1 st b₃ = [.b₁,b₂.[ holds
Int b₃ = ].b₁,b₂.[

proof end;

theorem Th51: :: RCOMP_3:51

for b₁, b₂ being real number
for b₃ being Subset of R^1 st b₃ = ].b₁,b₂.] holds
Int b₃ = ].b₁,b₂.[

proof end;

registration

let c₁ be convex Subset of R^1 ;
cluster R^1 | a₁ -> convex ;
coherence

proof end;

end;

registration

let c₁ be connected Subset of REAL ;
cluster R^1 a₁ -> convex ;
coherence

proof end;

end;

theorem Th52: :: RCOMP_3:52

for b₁ being Subset of R^1
for b₂ being Subset of REAL st b₁ = b₂ holds
( b₁ is connected iff b₂ is connected )

proof end;

registration

let c₁ be real number ;
cluster Closed-Interval-TSpace a₁,a₁ -> trivial ;
coherence

proof end;

end;

theorem Th53: :: RCOMP_3:53

for b₁, b₂ being real number st b₁ <= b₂ holds
for b₃ being Subset of (Closed-Interval-TSpace b₁,b₂) holds b₃ is bounded Subset of REAL

proof end;

theorem Th54: :: RCOMP_3:54

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ holds
for b₅ being Subset of (Closed-Interval-TSpace b₁,b₂) st b₅ = [.b₃,b₄.[ & b₁ < b₃ & b₄ <= b₂ holds
Int b₅ = ].b₃,b₄.[

proof end;

theorem Th55: :: RCOMP_3:55

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ holds
for b₅ being Subset of (Closed-Interval-TSpace b₁,b₂) st b₅ = ].b₃,b₄.] & b₁ <= b₃ & b₄ < b₂ holds
Int b₅ = ].b₃,b₄.[

proof end;

theorem Th56: :: RCOMP_3:56

for b₁, b₂ being real number
for b₃ being Subset of (Closed-Interval-TSpace b₁,b₂)
for b₄ being Subset of REAL st b₃ = b₄ holds
( b₃ is connected iff b₄ is connected )

proof end;

registration

let c₁ be TopSpace;
cluster open closed connected Element of K10(the carrier of a₁);
existence

proof end;

end;

registration

let c₁ be non empty connected TopSpace;
cluster non empty open closed connected Element of K10(the carrier of a₁);
existence

proof end;

end;

theorem Th57: :: RCOMP_3:57

for b₁, b₂ being real number st b₁ <= b₂ holds
for b₃ being open connected Subset of (Closed-Interval-TSpace b₁,b₂) holds
( b₃ is empty or b₃ = [.b₁,b₂.] or ex b₄ being real number st
( b₁ < b₄ & b₄ <= b₂ & b₃ = [.b₁,b₄.[ ) or ex b₄ being real number st
( b₁ <= b₄ & b₄ < b₂ & b₃ = ].b₄,b₂.] ) or ex b₄, b₅ being real number st
( b₁ <= b₄ & b₄ < b₅ & b₅ <= b₂ & b₃ = ].b₄,b₅.[ ) )

proof end;

deffunc H₁( set ) -> set = a₁;

defpred S₁[ set , set ] means a₁ c= a₂;

theorem Th58: :: RCOMP_3:58

for b₁ being 1-sorted
for b₂ being Subset-Family of b₁ holds
( b₂ is_a_cover_of b₁ iff b₂ is_a_cover_of [#] b₁ )

proof end;

theorem Th59: :: RCOMP_3:59

for b₁ being 1-sorted
for b₂ being finite Subset-Family of b₁
for b₃ being Subset-Family of b₁ st b₂ is_a_cover_of b₁ & b₃ = b₂ \ { b₄ where B is Subset of b₁ : ( b₄ in b₂ & ex b₁ being Subset of b₁ st
( b₅ in b₂ & b₄ c= b₅ & b₄ <> b₅ ) ) } holds
b₃ is_a_cover_of b₁

proof end;

theorem Th60: :: RCOMP_3:60

for b₁ being non empty trivial 1-sorted
for b₂ being Point of b₁
for b₃ being Subset-Family of b₁ st b₃ is_a_cover_of b₁ holds
{b₂} in b₃

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset-Family of c₁;
attr a₂ is connected means :Def1: :: RCOMP_3:def 1
for b₁ being Subset of a₁ st b₁ in a₂ holds
b₁ is connected;

end;

:: deftheorem Def1 defines connected RCOMP_3:def 1 :

registration

let c₁ be TopSpace;
cluster non empty open closed connected Element of K10(K10(the carrier of a₁));
existence

proof end;

end;

Lemma55: for b₁, b₂ being real number
for b₃ being Subset-Family of (Closed-Interval-TSpace b₁,b₂) st [.b₁,b₂.] in b₃ & b₁ <= b₂ holds
( rng <*[.b₁,b₂.]*> c= b₃ & union (rng <*[.b₁,b₂.]*>) = [.b₁,b₂.] & ( for b₄ being natural number st 1 <= b₄ holds
( ( b₄ <= len <*[.b₁,b₂.]*> implies not <*[.b₁,b₂.]*> /. b₄ is empty ) & ( b₄ + 1 <= len <*[.b₁,b₂.]*> implies ( inf (<*[.b₁,b₂.]*> /. b₄) <= inf (<*[.b₁,b₂.]*> /. (b₄ + 1)) & sup (<*[.b₁,b₂.]*> /. b₄) <= sup (<*[.b₁,b₂.]*> /. (b₄ + 1)) & inf (<*[.b₁,b₂.]*> /. (b₄ + 1)) < sup (<*[.b₁,b₂.]*> /. b₄) ) ) & ( b₄ + 2 <= len <*[.b₁,b₂.]*> implies sup (<*[.b₁,b₂.]*> /. b₄) <= inf (<*[.b₁,b₂.]*> /. (b₄ + 2)) ) ) ) )

proof end;

theorem Th61: :: RCOMP_3:61

for b₁ being TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ is_a_cover_of b₁ & b₂ is finite holds
for b₄ being set st b₃ = b₂ \ { b₅ where B is Subset of b₁ : ( b₅ in b₂ & ex b₁ being Subset of b₁ st
( b₆ in b₂ & b₅ c= b₆ & b₅ <> b₆ ) ) } & b₄ = { b₅ where B is Subset-Family of b₁ : ( b₅ is_a_cover_of b₁ & b₅ c= b₃ ) } holds
b₄ has_lower_Zorn_property_wrt RelIncl b₄

proof end;

theorem Th62: :: RCOMP_3:62

for b₁ being TopSpace
for b₂, b₃ being set st b₃ = { b₄ where B is Subset-Family of b₁ : ( b₄ is_a_cover_of b₁ & b₄ c= b₂ ) } holds
for b₄ being set st b₄ is_minimal_in RelIncl b₃ & b₄ in field (RelIncl b₃) holds
for b₅ being Subset of b₁ st b₅ in b₄ holds
for b₆, b₇ being Subset of b₁ holds
( not b₆ in b₄ or not b₇ in b₄ or not b₅ c= b₆ \/ b₇ or not b₅ <> b₆ or not b₅ <> b₇ )

proof end;

definition

let c₁, c₂ be real number ;
let c₃ be Subset-Family of (Closed-Interval-TSpace c₁,c₂);
assume that
E58: c₃ is_a_cover_of Closed-Interval-TSpace c₁,c₂ and
E59: c₃ is open and
E60: c₃ is connected and
E61: c₁ <= c₂ ;
mode IntervalCover of c₃ -> FinSequence of bool REAL means :Def2: :: RCOMP_3:def 2
( rng a₄ c= a₃ & union (rng a₄) = [.a₁,a₂.] & ( for b₁ being natural number st 1 <= b₁ holds
( ( b₁ <= len a₄ implies not a₄ /. b₁ is empty ) & ( b₁ + 1 <= len a₄ implies ( inf (a₄ /. b₁) <= inf (a₄ /. (b₁ + 1)) & sup (a₄ /. b₁) <= sup (a₄ /. (b₁ + 1)) & inf (a₄ /. (b₁ + 1)) < sup (a₄ /. b₁) ) ) & ( b₁ + 2 <= len a₄ implies sup (a₄ /. b₁) <= inf (a₄ /. (b₁ + 2)) ) ) ) & ( [.a₁,a₂.] in a₃ implies a₄ = <*[.a₁,a₂.]*> ) & ( not [.a₁,a₂.] in a₃ implies ( ex b₁ being real number st
( a₁ < b₁ & b₁ <= a₂ & a₄ . 1 = [.a₁,b₁.[ ) & ex b₁ being real number st
( a₁ <= b₁ & b₁ < a₂ & a₄ . (len a₄) = ].b₁,a₂.] ) & ( for b₁ being natural number st 1 < b₁ & b₁ < len a₄ holds
ex b₂, b₃ being real number st
( a₁ <= b₂ & b₂ < b₃ & b₃ <= a₂ & a₄ . b₁ = ].b₂,b₃.[ ) ) ) ) );
existence

proof end;

end;

:: deftheorem Def2 defines IntervalCover RCOMP_3:def 2 :

theorem Th63: :: RCOMP_3:63

for b₁, b₂ being real number
for b₃ being Subset-Family of (Closed-Interval-TSpace b₁,b₂) st b₃ is_a_cover_of Closed-Interval-TSpace b₁,b₂ & b₃ is open & b₃ is connected & b₁ <= b₂ & [.b₁,b₂.] in b₃ holds
<*[.b₁,b₂.]*> is IntervalCover of b₃

proof end;

theorem Th64: :: RCOMP_3:64

for b₁ being real number
for b₂ being Subset-Family of (Closed-Interval-TSpace b₁,b₁)
for b₃ being IntervalCover of b₂ st b₂ is_a_cover_of Closed-Interval-TSpace b₁,b₁ & b₂ is open & b₂ is connected holds
b₃ = <*[.b₁,b₁.]*>

proof end;

theorem Th65: :: RCOMP_3:65

for b₁, b₂ being real number
for b₃ being Subset-Family of (Closed-Interval-TSpace b₁,b₂)
for b₄ being IntervalCover of b₃ st b₃ is_a_cover_of Closed-Interval-TSpace b₁,b₂ & b₃ is open & b₃ is connected & b₁ <= b₂ holds
1 <= len b₄

proof end;

theorem Th66: :: RCOMP_3:66

proof end;

theorem Th67: :: RCOMP_3:67

for b₁, b₂ being real number
for b₃, b₄ being natural number
for b₅ being Subset-Family of (Closed-Interval-TSpace b₁,b₂)
for b₆ being IntervalCover of b₅ st b₅ is_a_cover_of Closed-Interval-TSpace b₁,b₂ & b₅ is open & b₅ is connected & b₁ <= b₂ & b₃ in dom b₆ & b₄ in dom b₆ & b₃ < b₄ holds
inf (b₆ /. b₃) <= inf (b₆ /. b₄)

proof end;

theorem Th68: :: RCOMP_3:68

proof end;

theorem Th69: :: RCOMP_3:69

for b₁, b₂ being real number
for b₃ being natural number
for b₄ being Subset-Family of (Closed-Interval-TSpace b₁,b₂)
for b₅ being IntervalCover of b₄ st b₄ is_a_cover_of Closed-Interval-TSpace b₁,b₂ & b₄ is open & b₄ is connected & b₁ <= b₂ & 1 <= b₃ & b₃ + 1 <= len b₅ holds
not ].(inf (b₅ /. (b₃ + 1))),(sup (b₅ /. b₃)).[ is empty

proof end;

theorem Th70: :: RCOMP_3:70

proof end;

theorem Th71: :: RCOMP_3:71

proof end;

theorem Th72: :: RCOMP_3:72

proof end;

theorem Th73: :: RCOMP_3:73

proof end;

definition

let c₁, c₂ be real number ;
let c₃ be Subset-Family of (Closed-Interval-TSpace c₁,c₂);
let c₄ be IntervalCover of c₃;
assume that
E65: c₃ is_a_cover_of Closed-Interval-TSpace c₁,c₂ and
E66: c₃ is open and
E67: c₃ is connected and
E68: c₁ <= c₂ ;
mode IntervalCoverPts of c₄ -> FinSequence of REAL means :Def3: :: RCOMP_3:def 3
( len a₅ = (len a₄) + 1 & a₅ . 1 = a₁ & a₅ . (len a₅) = a₂ & ( for b₁ being natural number st 1 <= b₁ & b₁ + 1 < len a₅ holds
a₅ . (b₁ + 1) in ].(inf (a₄ /. (b₁ + 1))),(sup (a₄ /. b₁)).[ ) );
existence

proof end;

end;

:: deftheorem Def3 defines IntervalCoverPts RCOMP_3:def 3 :

theorem Th74: :: RCOMP_3:74

for b₁, b₂ being real number
for b₃ being Subset-Family of (Closed-Interval-TSpace b₁,b₂)
for b₄ being IntervalCover of b₃
for b₅ being IntervalCoverPts of b₄ st b₃ is_a_cover_of Closed-Interval-TSpace b₁,b₂ & b₃ is open & b₃ is connected & b₁ <= b₂ holds
2 <= len b₅

proof end;

theorem Th75: :: RCOMP_3:75

proof end;

theorem Th76: :: RCOMP_3:76

for b₁, b₂ being real number
for b₃ being natural number
for b₄ being Subset-Family of (Closed-Interval-TSpace b₁,b₂)
for b₅ being IntervalCover of b₄
for b₆ being IntervalCoverPts of b₅ st b₄ is_a_cover_of Closed-Interval-TSpace b₁,b₂ & b₄ is open & b₄ is connected & b₁ <= b₂ & 1 <= b₃ & b₃ + 1 < len b₆ holds
b₆ . (b₃ + 1) < sup (b₅ /. b₃)

proof end;

theorem Th77: :: RCOMP_3:77

for b₁, b₂ being real number
for b₃ being natural number
for b₄ being Subset-Family of (Closed-Interval-TSpace b₁,b₂)
for b₅ being IntervalCover of b₄
for b₆ being IntervalCoverPts of b₅ st b₄ is_a_cover_of Closed-Interval-TSpace b₁,b₂ & b₄ is open & b₄ is connected & b₁ <= b₂ & 1 < b₃ & b₃ <= len b₅ holds
inf (b₅ /. b₃) < b₆ . b₃

proof end;

theorem Th78: :: RCOMP_3:78

for b₁, b₂ being real number
for b₃ being natural number
for b₄ being Subset-Family of (Closed-Interval-TSpace b₁,b₂)
for b₅ being IntervalCover of b₄
for b₆ being IntervalCoverPts of b₅ st b₄ is_a_cover_of Closed-Interval-TSpace b₁,b₂ & b₄ is open & b₄ is connected & b₁ <= b₂ & 1 <= b₃ & b₃ < len b₅ holds
b₆ . b₃ <= inf (b₅ /. (b₃ + 1))

proof end;

theorem Th79: :: RCOMP_3:79

proof end;

theorem Th80: :: RCOMP_3:80

for b₁, b₂ being real number
for b₃ being natural number
for b₄ being Subset-Family of (Closed-Interval-TSpace b₁,b₂)
for b₅ being IntervalCover of b₄
for b₆ being IntervalCoverPts of b₅ st b₄ is_a_cover_of Closed-Interval-TSpace b₁,b₂ & b₄ is open & b₄ is connected & b₁ <= b₂ & 1 <= b₃ & b₃ < len b₆ holds
[.(b₆ . b₃),(b₆ . (b₃ + 1)).] c= b₅ . b₃

proof end;