:: BORSUK_5 semantic presentation

theorem Th1: :: BORSUK_5:1

canceled;

theorem Th2: :: BORSUK_5:2

for b₁, b₂, b₃ being set st b₁ c= b₂ & b₂ c= b₁ \/ {b₃} & not b₁ \/ {b₃} = b₂ holds
b₁ = b₂

proof end;

theorem Th3: :: BORSUK_5:3

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds {b₁,b₂,b₃,b₄,b₅,b₆} = {b₁,b₃,b₆} \/ {b₂,b₄,b₅}

proof end;

definition

let c₁, c₂, c₃, c₄, c₅, c₆ be set ;
pred c₁,c₂,c₃,c₄,c₅,c₆ are_mutually_different means :Def1: :: BORSUK_5:def 1
( a₁ <> a₂ & a₁ <> a₃ & a₁ <> a₄ & a₁ <> a₅ & a₁ <> a₆ & a₂ <> a₃ & a₂ <> a₄ & a₂ <> a₅ & a₂ <> a₆ & a₃ <> a₄ & a₃ <> a₅ & a₃ <> a₆ & a₄ <> a₅ & a₄ <> a₆ & a₅ <> a₆ );

end;

:: deftheorem Def1 defines are_mutually_different BORSUK_5:def 1 :

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇ be set ;
pred c₁,c₂,c₃,c₄,c₅,c₆,c₇ are_mutually_different means :Def2: :: BORSUK_5:def 2
( a₁ <> a₂ & a₁ <> a₃ & a₁ <> a₄ & a₁ <> a₅ & a₁ <> a₆ & a₁ <> a₇ & a₂ <> a₃ & a₂ <> a₄ & a₂ <> a₅ & a₂ <> a₆ & a₂ <> a₇ & a₃ <> a₄ & a₃ <> a₅ & a₃ <> a₆ & a₃ <> a₇ & a₄ <> a₅ & a₄ <> a₆ & a₄ <> a₇ & a₅ <> a₆ & a₅ <> a₇ & a₆ <> a₇ );

end;

:: deftheorem Def2 defines are_mutually_different BORSUK_5:def 2 :

theorem Th4: :: BORSUK_5:4

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁,b₂,b₃,b₄,b₅,b₆ are_mutually_different holds
card {b₁,b₂,b₃,b₄,b₅,b₆} = 6

proof end;

theorem Th5: :: BORSUK_5:5

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st b₁,b₂,b₃,b₄,b₅,b₆,b₇ are_mutually_different holds
card {b₁,b₂,b₃,b₄,b₅,b₆,b₇} = 7

proof end;

theorem Th6: :: BORSUK_5:6

for b₁, b₂, b₃, b₄, b₅, b₆ being set st {b₁,b₂,b₃} misses {b₄,b₅,b₆} holds
( b₁ <> b₄ & b₁ <> b₅ & b₁ <> b₆ & b₂ <> b₄ & b₂ <> b₅ & b₂ <> b₆ & b₃ <> b₄ & b₃ <> b₅ & b₃ <> b₆ )

proof end;

theorem Th7: :: BORSUK_5:7

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁,b₂,b₃ are_mutually_different & b₄,b₅,b₆ are_mutually_different & {b₁,b₂,b₃} misses {b₄,b₅,b₆} holds
b₁,b₂,b₃,b₄,b₅,b₆ are_mutually_different

proof end;

theorem Th8: :: BORSUK_5:8

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st b₁,b₂,b₃,b₄,b₅,b₆ are_mutually_different & {b₁,b₂,b₃,b₄,b₅,b₆} misses {b₇} holds
b₁,b₂,b₃,b₄,b₅,b₆,b₇ are_mutually_different

proof end;

theorem Th9: :: BORSUK_5:9

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st b₁,b₂,b₃,b₄,b₅,b₆,b₇ are_mutually_different holds
b₇,b₁,b₂,b₃,b₄,b₅,b₆ are_mutually_different

proof end;

theorem Th10: :: BORSUK_5:10

for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being set st b₁,b₂,b₃,b₄,b₅,b₆,b₇ are_mutually_different holds
b₁,b₂,b₅,b₃,b₆,b₇,b₄ are_mutually_different

proof end;

theorem Th11: :: BORSUK_5:11

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁ st ex b₄ being Function of I[01] ,b₁ st
( b₄ is continuous & b₄ . 0 = b₂ & b₄ . 1 = b₃ ) holds
ex b₄ being Function of I[01] ,b₁ st
( b₄ is continuous & b₄ . 0 = b₃ & b₄ . 1 = b₂ )

proof end;

Lemma7: R^1 is arcwise_connected

proof end;

registration

cluster R^1 -> arcwise_connected ;
coherence by Lemma7;

end;

registration

cluster non empty connected TopStruct ;
existence

proof end;

end;

theorem Th12: :: BORSUK_5:12

canceled;

theorem Th13: :: BORSUK_5:13

[#] R^1 = REAL by PRE_TOPC:def 3, TOPMETR:24;

notation

let c₁ be real number ;
synonym ].-infty,c₁.] for left_closed_halfline c₁;
synonym ].-infty,c₁.[ for left_open_halfline c₁;
synonym [.c₁,+infty.[ for right_closed_halfline c₁;
synonym ].c₁,+infty.[ for right_open_halfline c₁;

end;

theorem Th14: :: BORSUK_5:14

for b₁, b₂ being real number holds
( b₁ in ].b₂,+infty.[ iff b₁ > b₂ )

proof end;

theorem Th15: :: BORSUK_5:15

for b₁, b₂ being real number holds
( b₁ in [.b₂,+infty.[ iff b₁ >= b₂ )

proof end;

theorem Th16: :: BORSUK_5:16

for b₁, b₂ being real number holds
( b₁ in ].-infty,b₂.] iff b₁ <= b₂ )

proof end;

theorem Th17: :: BORSUK_5:17

for b₁, b₂ being real number holds
( b₁ in ].-infty,b₂.[ iff b₁ < b₂ )

proof end;

theorem Th18: :: BORSUK_5:18

for b₁ being real number holds REAL \ {b₁} = ].-infty,b₁.[ \/ ].b₁,+infty.[

proof end;

theorem Th19: :: BORSUK_5:19

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

proof end;

theorem Th20: :: BORSUK_5:20

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

proof end;

theorem Th21: :: BORSUK_5:21

for b₁, b₂ being Subset of R^1
for b₃, b₄, b₅, b₆ being real number st b₃ < b₄ & b₄ <= b₅ & b₅ < b₆ & b₁ = [.b₃,b₄.[ & b₂ = ].b₅,b₆.] holds
b₁,b₂ are_separated

proof end;

Lemma16: for b₁ being real number holds REAL \ ].-infty,b₁.[ = [.b₁,+infty.[
by LIMFUNC1:24;

Lemma17: for b₁ being real number holds REAL \ ].-infty,b₁.] = ].b₁,+infty.[
by LIMFUNC1:24;

Lemma18: for b₁ being real number holds REAL \ [.b₁,+infty.[ = ].-infty,b₁.[
by LIMFUNC1:24;

theorem Th22: :: BORSUK_5:22

canceled;

theorem Th23: :: BORSUK_5:23

canceled;

theorem Th24: :: BORSUK_5:24

canceled;

theorem Th25: :: BORSUK_5:25

canceled;

theorem Th26: :: BORSUK_5:26

for b₁ being real number holds ].-infty,b₁.] misses ].b₁,+infty.[

proof end;

theorem Th27: :: BORSUK_5:27

for b₁ being real number holds ].-infty,b₁.[ misses [.b₁,+infty.[

proof end;

theorem Th28: :: BORSUK_5:28

for b₁, b₂, b₃ being real number st b₁ <= b₃ & b₃ <= b₂ holds
[.b₁,b₂.] \/ [.b₃,+infty.[ = [.b₁,+infty.[

proof end;

theorem Th29: :: BORSUK_5:29

for b₁, b₂, b₃ being real number st b₁ <= b₃ & b₃ <= b₂ holds
].-infty,b₃.] \/ [.b₁,b₂.] = ].-infty,b₂.]

proof end;

registration

cluster -> real Element of RAT ;
coherence ;

end;

registration

cluster -> real Element of the carrier of RealSpace ;
coherence by METRIC_1:def 14, XREAL_0:def 1;

end;

theorem Th30: :: BORSUK_5:30

canceled;

theorem Th31: :: BORSUK_5:31

canceled;

theorem Th32: :: BORSUK_5:32

canceled;

theorem Th33: :: BORSUK_5:33

for b₁ being Subset of R^1
for b₂ being Point of RealSpace holds
( b₂ in Cl b₁ iff for b₃ being real number st b₃ > 0 holds
Ball b₂,b₃ meets b₁ ) by HAUSDORF:7, TOPMETR:def 7;

theorem Th34: :: BORSUK_5:34

for b₁, b₂ being Element of RealSpace st b₂ >= b₁ holds
dist b₁,b₂ = b₂ - b₁

proof end;

theorem Th35: :: BORSUK_5:35

for b₁ being Subset of R^1 st b₁ = RAT holds
Cl b₁ = the carrier of R^1

proof end;

theorem Th36: :: BORSUK_5:36

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

proof end;

registration

cluster number_e -> irrational ;
coherence by IRRAT_1:42;

end;

definition

func IRRAT -> Subset of REAL equals :: BORSUK_5:def 3
REAL \ RAT ;
coherence by XBOOLE_1:36;

end;

:: deftheorem Def3 defines IRRAT BORSUK_5:def 3 :

definition

let c₁, c₂ be real number ;
func RAT c₁,c₂ -> Subset of REAL equals :: BORSUK_5:def 4
RAT /\ ].a₁,a₂.[;
coherence

proof end;

func IRRAT c₁,c₂ -> Subset of REAL equals :: BORSUK_5:def 5
IRRAT /\ ].a₁,a₂.[;
coherence ;

end;

:: deftheorem Def4 defines RAT BORSUK_5:def 4 :

:: deftheorem Def5 defines IRRAT BORSUK_5:def 5 :

theorem Th37: :: BORSUK_5:37

for b₁ being real number holds
( b₁ is irrational iff b₁ in IRRAT )

proof end;

registration

cluster real irrational set ;
existence by IRRAT_1:42;

end;

registration

cluster IRRAT -> non empty ;
coherence by Th37, IRRAT_1:42;

end;

theorem Th38: :: BORSUK_5:38

for b₁ being rational number
for b₂ being real irrational number holds b₁ + b₂ is irrational

proof end;

theorem Th39: :: BORSUK_5:39

for b₁ being real irrational number holds - b₁ is irrational

proof end;

theorem Th40: :: BORSUK_5:40

for b₁ being rational number
for b₂ being real irrational number holds b₁ - b₂ is irrational

proof end;

theorem Th41: :: BORSUK_5:41

for b₁ being rational number
for b₂ being real irrational number holds b₂ - b₁ is irrational

proof end;

theorem Th42: :: BORSUK_5:42

for b₁ being rational number
for b₂ being real irrational number st b₁ <> 0 holds
b₁ * b₂ is irrational

proof end;

theorem Th43: :: BORSUK_5:43

for b₁ being rational number
for b₂ being real irrational number st b₁ <> 0 holds
b₂ / b₁ is irrational

proof end;

registration

cluster real irrational -> non zero real set ;
coherence

proof end;

end;

theorem Th44: :: BORSUK_5:44

for b₁ being rational number
for b₂ being real irrational number st b₁ <> 0 holds
b₁ / b₂ is irrational

proof end;

theorem Th45: :: BORSUK_5:45

for b₁ being real irrational number holds frac b₁ is irrational

proof end;

registration

let c₁ be real irrational number ;
cluster frac a₁ -> non zero irrational ;
coherence by Th45;

end;

registration

let c₁ be real irrational number ;
cluster - a₁ -> non zero irrational ;
coherence by Th39;

end;

registration

let c₁ be rational number ;
let c₂ be real irrational number ;
cluster a₁ + a₂ -> non zero irrational ;
coherence by Th38;
cluster a₂ + a₁ -> non zero irrational ;
coherence ;
cluster a₁ - a₂ -> non zero irrational ;
coherence by Th40;
cluster a₂ - a₁ -> non zero irrational ;
coherence by Th41;

end;

registration

cluster non zero rational set ;
existence

proof end;

end;

registration

let c₁ be non zero rational number ;
let c₂ be real irrational number ;
cluster a₁ * a₂ -> non zero irrational ;
coherence by Th42;
cluster a₂ * a₁ -> non zero irrational ;
coherence ;
cluster a₁ / a₂ -> non zero irrational ;
coherence by Th44;
cluster a₂ / a₁ -> non zero irrational ;
coherence by Th43;

end;

theorem Th46: :: BORSUK_5:46

canceled;

theorem Th47: :: BORSUK_5:47

for b₁, b₂ being real number st b₁ < b₂ holds
ex b₃, b₄ being rational number st
( b₁ < b₃ & b₃ < b₄ & b₄ < b₂ )

proof end;

Lemma36: for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₁ < b₃ & 0 < b₄ & b₄ < 1 holds
b₁ < ((1 - b₄) * b₂) + (b₄ * b₃)
by XREAL_1:179;

Lemma37: for b₁, b₂, b₃, b₄ being real number st b₂ < b₁ & b₃ <= b₁ & 0 < b₄ & b₄ < 1 holds
((1 - b₄) * b₂) + (b₄ * b₃) < b₁
by XREAL_1:180;

theorem Th48: :: BORSUK_5:48

canceled;

theorem Th49: :: BORSUK_5:49

canceled;

theorem Th50: :: BORSUK_5:50

for b₁, b₂ being real number st b₁ < b₂ holds
ex b₃ being real irrational number st
( b₁ < b₃ & b₃ < b₂ )

proof end;

theorem Th51: :: BORSUK_5:51

for b₁ being Subset of R^1 st b₁ = IRRAT holds
Cl b₁ = the carrier of R^1

proof end;

Lemma40: for b₁ being Subset of R^1
for b₂, b₃ being real number st b₂ < b₃ & b₁ = RAT b₂,b₃ holds
( b₂ in Cl b₁ & b₃ in Cl b₁ )

proof end;

Lemma41: for b₁ being Subset of R^1
for b₂, b₃ being real number st b₂ < b₃ & b₁ = IRRAT b₂,b₃ holds
( b₂ in Cl b₁ & b₃ in Cl b₁ )

proof end;

theorem Th52: :: BORSUK_5:52

for b₁, b₂, b₃ being real number st b₁ < b₂ holds
( b₃ in RAT b₁,b₂ iff ( not b₃ is irrational & b₁ < b₃ & b₃ < b₂ ) )

proof end;

theorem Th53: :: BORSUK_5:53

for b₁, b₂, b₃ being real number st b₁ < b₂ holds
( b₃ in IRRAT b₁,b₂ iff ( b₃ is irrational & b₁ < b₃ & b₃ < b₂ ) )

proof end;

theorem Th54: :: BORSUK_5:54

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

proof end;

theorem Th55: :: BORSUK_5:55

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

proof end;

theorem Th56: :: BORSUK_5:56

for b₁ being connected TopSpace
for b₂ being open closed Subset of b₁ holds
( b₂ = {} or b₂ = [#] b₁ )

proof end;

theorem Th57: :: BORSUK_5:57

for b₁ being Subset of R^1 st b₁ is closed & b₁ is open & not b₁ = {} holds
b₁ = REAL

proof end;

theorem Th58: :: BORSUK_5:58

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

proof end;

theorem Th59: :: BORSUK_5:59

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

proof end;

theorem Th60: :: BORSUK_5:60

for b₁ being Subset of R^1
for b₂, b₃, b₄ being real number st b₁ = [.b₂,b₃.[ \/ ].b₃,b₄.] & b₂ < b₃ & b₃ < b₄ holds
Cl b₁ = [.b₂,b₄.]

proof end;

theorem Th61: :: BORSUK_5:61

for b₁ being Subset of R^1
for b₂ being real number st b₁ = {b₂} holds
Cl b₁ = {b₂}

proof end;

theorem Th62: :: BORSUK_5:62

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

proof end;

Lemma52: for b₁ being real number holds ].b₁,+infty.[ is open
by FCONT_3:7;

Lemma53: for b₁ being real number holds ].-infty,b₁.] is closed
by FCONT_3:6;

Lemma54: for b₁ being real number holds ].-infty,b₁.[ is open
by FCONT_3:8;

Lemma55: for b₁ being real number holds [.b₁,+infty.[ is closed
by FCONT_3:5;

theorem Th63: :: BORSUK_5:63

for b₁ being Subset of R^1
for b₂ being real number st b₁ = ].b₂,+infty.[ holds
b₁ is open

proof end;

theorem Th64: :: BORSUK_5:64

for b₁ being Subset of R^1
for b₂ being real number st b₁ = ].-infty,b₂.[ holds
b₁ is open

proof end;

theorem Th65: :: BORSUK_5:65

for b₁ being Subset of R^1
for b₂ being real number st b₁ = ].-infty,b₂.] holds
b₁ is closed

proof end;

theorem Th66: :: BORSUK_5:66

for b₁ being Subset of R^1
for b₂ being real number st b₁ = [.b₂,+infty.[ holds
b₁ is closed

proof end;

theorem Th67: :: BORSUK_5:67

for b₁ being real number holds [.b₁,+infty.[ = {b₁} \/ ].b₁,+infty.[

proof end;

theorem Th68: :: BORSUK_5:68

for b₁ being real number holds ].-infty,b₁.] = {b₁} \/ ].-infty,b₁.[

proof end;

Lemma62: for b₁ being real number holds ].b₁,+infty.[ c= [.b₁,+infty.[
by LIMFUNC1:10;

Lemma63: for b₁ being real number holds ].-infty,b₁.[ c= ].-infty,b₁.]
by LIMFUNC1:15;

registration

let c₁ be real number ;
cluster ].a₁,+infty.[ -> non empty ;
coherence

proof end;

cluster ].-infty,a₁.] -> non empty ;
coherence by Th16;
cluster ].-infty,a₁.[ -> non empty ;
coherence

proof end;

cluster [.a₁,+infty.[ -> non empty ;
coherence by Th15;

end;

theorem Th69: :: BORSUK_5:69

canceled;

theorem Th70: :: BORSUK_5:70

canceled;

theorem Th71: :: BORSUK_5:71

for b₁ being real number holds ].b₁,+infty.[ <> REAL

proof end;

theorem Th72: :: BORSUK_5:72

for b₁ being real number holds [.b₁,+infty.[ <> REAL

proof end;

theorem Th73: :: BORSUK_5:73

for b₁ being real number holds ].-infty,b₁.] <> REAL

proof end;

theorem Th74: :: BORSUK_5:74

for b₁ being real number holds ].-infty,b₁.[ <> REAL

proof end;

theorem Th75: :: BORSUK_5:75

for b₁ being Subset of R^1
for b₂ being real number st b₁ = ].b₂,+infty.[ holds
Cl b₁ = [.b₂,+infty.[

proof end;

theorem Th76: :: BORSUK_5:76

for b₁ being real number holds Cl ].b₁,+infty.[ = [.b₁,+infty.[

proof end;

theorem Th77: :: BORSUK_5:77

for b₁ being Subset of R^1
for b₂ being real number st b₁ = ].-infty,b₂.[ holds
Cl b₁ = ].-infty,b₂.]

proof end;

theorem Th78: :: BORSUK_5:78

for b₁ being real number holds Cl ].-infty,b₁.[ = ].-infty,b₁.]

proof end;

theorem Th79: :: BORSUK_5:79

for b₁, b₂ being Subset of R^1
for b₃ being real number st b₁ = ].-infty,b₃.[ & b₂ = ].b₃,+infty.[ holds
b₁,b₂ are_separated

proof end;

theorem Th80: :: BORSUK_5:80

for b₁ being Subset of R^1
for b₂, b₃ being real number st b₂ < b₃ & b₁ = [.b₂,b₃.[ \/ ].b₃,+infty.[ holds
Cl b₁ = [.b₂,+infty.[

proof end;

theorem Th81: :: BORSUK_5:81

for b₁ being Subset of R^1
for b₂, b₃ being real number st b₂ < b₃ & b₁ = ].b₂,b₃.[ \/ ].b₃,+infty.[ holds
Cl b₁ = [.b₂,+infty.[

proof end;

theorem Th82: :: BORSUK_5:82

for b₁ being Subset of R^1
for b₂, b₃, b₄ being real number st b₂ < b₃ & b₃ < b₄ & b₁ = ((RAT b₂,b₃) \/ ].b₃,b₄.[) \/ ].b₄,+infty.[ holds
Cl b₁ = [.b₂,+infty.[

proof end;

theorem Th83: :: BORSUK_5:83

for b₁ being Subset of R^1 holds b₁ ` = REAL \ b₁ by Th13, PRE_TOPC:17;

theorem Th84: :: BORSUK_5:84

for b₁, b₂ being real number st b₁ < b₂ holds
IRRAT b₁,b₂ misses RAT b₁,b₂

proof end;

Lemma71: for b₁, b₂ being real number st b₂ <= b₁ holds
RAT b₁,b₂ = {}

proof end;

Lemma72: for b₁, b₂ being real number st b₂ <= b₁ holds
REAL = ].-infty,b₁.] \/ [.b₂,+infty.[

proof end;

theorem Th85: :: BORSUK_5:85

for b₁, b₂ being real number holds REAL \ (RAT b₁,b₂) = (].-infty,b₁.] \/ (IRRAT b₁,b₂)) \/ [.b₂,+infty.[

proof end;

theorem Th86: :: BORSUK_5:86

for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₂ < b₃ holds
not b₁ in ].b₂,b₃.[ \/ ].b₃,+infty.[

proof end;

theorem Th87: :: BORSUK_5:87

for b₁, b₂ being real number st b₁ < b₂ holds
not b₂ in ].b₁,b₂.[ \/ ].b₂,+infty.[

proof end;

theorem Th88: :: BORSUK_5:88

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

proof end;

theorem Th89: :: BORSUK_5:89

for b₁ being Subset of R^1 st b₁ = ((RAT 2,4) \/ ].4,5.[) \/ ].5,+infty.[ holds
b₁ ` = ((].-infty,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}

proof end;

theorem Th90: :: BORSUK_5:90

for b₁ being Subset of R^1
for b₂ being real number st b₁ = {b₂} holds
b₁ ` = ].-infty,b₂.[ \/ ].b₂,+infty.[

proof end;

Lemma77: ((IRRAT 2,4) \/ {4}) \/ {5} c= ].1,+infty.[

proof end;

].1,+infty.[ c= [.1,+infty.[
by Lemma62;

then Lemma78: ((IRRAT 2,4) \/ {4}) \/ {5} c= [.1,+infty.[
by Lemma77, XBOOLE_1:1;

Lemma79: ].-infty,1.[ /\ (((].-infty,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}) = ].-infty,1.[

proof end;

theorem Th91: :: BORSUK_5:91

for b₁, b₂ being real number st b₁ < b₂ holds
].b₁,+infty.[ /\ ].-infty,b₂.] = ].b₁,b₂.]

proof end;

Lemma81: ].1,+infty.[ /\ (((].-infty,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}) = ((].1,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}

proof end;

theorem Th92: :: BORSUK_5:92

(].-infty,1.[ \/ ].1,+infty.[) /\ (((].-infty,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}) = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT 2,4)) \/ {4}) \/ {5}

proof end;

theorem Th93: :: BORSUK_5:93

for b₁, b₂ being real number st b₁ <= b₂ holds
].-infty,b₂.[ \ {b₁} = ].-infty,b₁.[ \/ ].b₁,b₂.[

proof end;

theorem Th94: :: BORSUK_5:94

for b₁, b₂ being real number st b₁ <= b₂ holds
].b₁,+infty.[ \ {b₂} = ].b₁,b₂.[ \/ ].b₂,+infty.[

proof end;

theorem Th95: :: BORSUK_5:95

for b₁ being Subset of R^1
for b₂, b₃ being real number st b₂ <= b₃ & b₁ = {b₂} \/ [.b₃,+infty.[ holds
b₁ ` = ].-infty,b₂.[ \/ ].b₂,b₃.[

proof end;

theorem Th96: :: BORSUK_5:96

for b₁ being Subset of R^1
for b₂, b₃ being real number st b₂ < b₃ & b₁ = ].-infty,b₂.[ \/ ].b₂,b₃.[ holds
Cl b₁ = ].-infty,b₃.]

proof end;

theorem Th97: :: BORSUK_5:97

for b₁ being Subset of R^1
for b₂, b₃ being real number st b₂ < b₃ & b₁ = ].-infty,b₂.[ \/ ].b₂,b₃.] holds
Cl b₁ = ].-infty,b₃.]

proof end;

theorem Th98: :: BORSUK_5:98

for b₁ being Subset of R^1
for b₂ being real number st b₁ = ].-infty,b₂.] holds
b₁ ` = ].b₂,+infty.[

proof end;

theorem Th99: :: BORSUK_5:99

for b₁ being Subset of R^1
for b₂ being real number st b₁ = [.b₂,+infty.[ holds
b₁ ` = ].-infty,b₂.[

proof end;

theorem Th100: :: BORSUK_5:100

for b₁ being Subset of R^1
for b₂, b₃, b₄ being real number st b₂ < b₃ & b₃ < b₄ & b₁ = ((].-infty,b₂.[ \/ ].b₂,b₃.]) \/ (IRRAT b₃,b₄)) \/ {b₄} holds
Cl b₁ = ].-infty,b₄.]

proof end;

theorem Th101: :: BORSUK_5:101

for b₁ being Subset of R^1
for b₂, b₃, b₄, b₅ being real number st b₂ < b₃ & b₃ < b₄ & b₁ = (((].-infty,b₂.[ \/ ].b₂,b₃.]) \/ (IRRAT b₃,b₄)) \/ {b₄}) \/ {b₅} holds
Cl b₁ = ].-infty,b₄.] \/ {b₅}

proof end;

theorem Th102: :: BORSUK_5:102

for b₁ being Subset of R^1
for b₂, b₃ being real number st b₂ <= b₃ & b₁ = ].-infty,b₂.] \/ {b₃} holds
b₁ ` = ].b₂,b₃.[ \/ ].b₃,+infty.[

proof end;

theorem Th103: :: BORSUK_5:103

for b₁, b₂ being real number holds [.b₁,+infty.[ \/ {b₂} <> REAL

proof end;

theorem Th104: :: BORSUK_5:104

for b₁, b₂ being real number holds ].-infty,b₁.] \/ {b₂} <> REAL

proof end;

theorem Th105: :: BORSUK_5:105

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st b₂ <> b₃ holds
b₂ ` <> b₃ `

proof end;

theorem Th106: :: BORSUK_5:106

for b₁ being Subset of R^1 st REAL = b₁ ` holds
b₁ = {}

proof end;

registration

cluster K384() -> arcwise_connected ;
coherence

proof end;

end;

theorem Th107: :: BORSUK_5:107

for b₁ being compact Subset of R^1
for b₂ being Subset of REAL st b₂ = b₁ holds
( b₂ is bounded_above & b₂ is bounded_below )

proof end;

theorem Th108: :: BORSUK_5:108

for b₁ being compact Subset of R^1
for b₂ being Subset of REAL
for b₃ being real number st b₃ in b₂ & b₂ = b₁ holds
( inf b₂ <= b₃ & b₃ <= sup b₂ )

proof end;

theorem Th109: :: BORSUK_5:109

for b₁ being non empty connected compact Subset of R^1
for b₂ being Subset of REAL st b₁ = b₂ & [.(inf b₂),(sup b₂).] c= b₂ holds
[.(inf b₂),(sup b₂).] = b₂

proof end;

theorem Th110: :: BORSUK_5:110

for b₁ being connected Subset of R^1
for b₂, b₃, b₄ being real number st b₂ <= b₃ & b₃ <= b₄ & b₂ in b₁ & b₄ in b₁ holds
b₃ in b₁

proof end;

theorem Th111: :: BORSUK_5:111

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

proof end;

theorem Th112: :: BORSUK_5:112

for b₁ being non empty connected compact Subset of R^1 holds b₁ is non empty closed-interval Subset of REAL

proof end;

theorem Th113: :: BORSUK_5:113

for b₁ being non empty connected compact Subset of R^1 ex b₂, b₃ being real number st
( b₂ <= b₃ & b₁ = [.b₂,b₃.] )

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset-Family of c₁;
attr a₂ is with_proper_subsets means :Def6: :: BORSUK_5:def 6
not the carrier of a₁ in a₂;

end;

:: deftheorem Def6 defines with_proper_subsets BORSUK_5:def 6 :

theorem Th114: :: BORSUK_5:114

for b₁ being TopStruct
for b₂, b₃ being Subset-Family of b₁ st b₂ is with_proper_subsets & b₃ c= b₂ holds
b₃ is with_proper_subsets

proof end;

registration

let c₁ be non empty TopStruct ;
cluster with_proper_subsets Element of K22(K22(the carrier of a₁));
existence

proof end;

end;

theorem Th115: :: BORSUK_5:115

for b₁ being non empty TopStruct
for b₂, b₃ being with_proper_subsets Subset-Family of b₁ holds b₂ \/ b₃ is with_proper_subsets

proof end;

registration

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

proof end;

end;