:: BORSUK_5 semantic presentation

theorem :: BORSUK_5:1

canceled;

theorem Th2: :: BORSUK_5:2

for A, B, a being set st A c= B & B c= A \/ {a} & not A \/ {a} = B holds
A = B

proof end;

theorem :: BORSUK_5:3

for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x3,x6} \/ {x2,x4,x5}

proof end;

definition

let x1, x2, x3, x4, x5, x6 be set ;
pred x1,x2,x3,x4,x5,x6 are_mutually_different means :Def1: :: BORSUK_5:def 1
( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x4 <> x5 & x4 <> x6 & x5 <> x6 );

end;

:: deftheorem Def1 defines are_mutually_different BORSUK_5:def 1 :

definition

let x1, x2, x3, x4, x5, x6, x7 be set ;
pred x1,x2,x3,x4,x5,x6,x7 are_mutually_different means :Def2: :: BORSUK_5:def 2
( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 & x4 <> x5 & x4 <> x6 & x4 <> x7 & x5 <> x6 & x5 <> x7 & x6 <> x7 );

end;

:: deftheorem Def2 defines are_mutually_different BORSUK_5:def 2 :

theorem Th4: :: BORSUK_5:4

for x1, x2, x3, x4, x5, x6 being set st x1,x2,x3,x4,x5,x6 are_mutually_different holds
card {x1,x2,x3,x4,x5,x6} = 6

proof end;

theorem :: BORSUK_5:5

for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6,x7 are_mutually_different holds
card {x1,x2,x3,x4,x5,x6,x7} = 7

proof end;

theorem Th6: :: BORSUK_5:6

for x1, x2, x3, x4, x5, x6 being set st {x1,x2,x3} misses {x4,x5,x6} holds
( x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 )

proof end;

theorem :: BORSUK_5:7

for x1, x2, x3, x4, x5, x6 being set st x1,x2,x3 are_mutually_different & x4,x5,x6 are_mutually_different & {x1,x2,x3} misses {x4,x5,x6} holds
x1,x2,x3,x4,x5,x6 are_mutually_different

proof end;

theorem :: BORSUK_5:8

for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6 are_mutually_different & {x1,x2,x3,x4,x5,x6} misses {x7} holds
x1,x2,x3,x4,x5,x6,x7 are_mutually_different

proof end;

theorem :: BORSUK_5:9

for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6,x7 are_mutually_different holds
x7,x1,x2,x3,x4,x5,x6 are_mutually_different

proof end;

theorem :: BORSUK_5:10

for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6,x7 are_mutually_different holds
x1,x2,x5,x3,x6,x7,x4 are_mutually_different

proof end;

theorem Th11: :: BORSUK_5:11

for T being non empty TopSpace
for a, b being Point of T st ex f being Function of I[01] ,T st
( f is continuous & f . 0 = a & f . 1 = b ) holds
ex g being Function of I[01] ,T st
( g is continuous & g . 0 = b & g . 1 = a )

proof end;

Lm1: R^1 is arcwise_connected

proof end;

registration

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

end;

registration

cluster non empty connected TopStruct ;
existence

proof end;

end;

theorem :: BORSUK_5:12

canceled;

theorem Th13: :: BORSUK_5:13

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

notation

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

end;

theorem Th14: :: BORSUK_5:14

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

proof end;

theorem Th15: :: BORSUK_5:15

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

proof end;

theorem Th16: :: BORSUK_5:16

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

proof end;

theorem Th17: :: BORSUK_5:17

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

proof end;

theorem Th18: :: BORSUK_5:18

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

proof end;

theorem Th19: :: BORSUK_5:19

for a, b, c, d being real number st a < b & b <= c holds
[.a,b.] misses ].c,d.]

proof end;

theorem Th20: :: BORSUK_5:20

for a, b, c, d being real number st a < b & b <= c holds
[.a,b.[ misses [.c,d.]

proof end;

theorem :: BORSUK_5:21

for A, B being Subset of R^1
for a, b, c, d being real number st a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] holds
A,B are_separated

proof end;

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

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

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

theorem :: BORSUK_5:22

canceled;

theorem :: BORSUK_5:23

canceled;

theorem :: BORSUK_5:24

canceled;

theorem :: BORSUK_5:25

canceled;

theorem Th26: :: BORSUK_5:26

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

proof end;

theorem Th27: :: BORSUK_5:27

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

proof end;

theorem Th28: :: BORSUK_5:28

for a, b, c being real number st a <= c & c <= b holds
[.a,b.] \/ [.c,+infty.[ = [.a,+infty.[

proof end;

theorem Th29: :: BORSUK_5:29

for a, b, c being real number st a <= c & c <= b holds
].-infty,c.] \/ [.a,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 :: BORSUK_5:30

canceled;

theorem :: BORSUK_5:31

canceled;

theorem :: BORSUK_5:32

canceled;

theorem :: BORSUK_5:33

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

theorem Th34: :: BORSUK_5:34

for p, q being Element of RealSpace st q >= p holds
dist p,q = q - p

proof end;

theorem Th35: :: BORSUK_5:35

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

proof end;

theorem Th36: :: BORSUK_5:36

for A being Subset of R^1
for a, b being real number st A = ].a,b.[ & a <> b holds
Cl A = [.a,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 defines IRRAT BORSUK_5:def 3 :

definition

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

proof end;

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

end;

:: deftheorem defines RAT BORSUK_5:def 4 :

:: deftheorem defines IRRAT BORSUK_5:def 5 :

theorem Th37: :: BORSUK_5:37

for x being real number holds
( x is irrational iff x 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 a being rational number
for b being real irrational number holds a + b is irrational

proof end;

theorem Th39: :: BORSUK_5:39

for a being real irrational number holds - a is irrational

proof end;

theorem Th40: :: BORSUK_5:40

for a being rational number
for b being real irrational number holds a - b is irrational

proof end;

theorem Th41: :: BORSUK_5:41

for a being rational number
for b being real irrational number holds b - a is irrational

proof end;

theorem Th42: :: BORSUK_5:42

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

proof end;

theorem Th43: :: BORSUK_5:43

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

proof end;

registration

cluster real irrational -> non zero real set ;
coherence

proof end;

end;

theorem Th44: :: BORSUK_5:44

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

proof end;

theorem Th45: :: BORSUK_5:45

for r being real irrational number holds frac r is irrational

proof end;

registration

let r be real irrational number ;
cluster frac r -> non zero irrational ;
coherence by Th45;

end;

registration

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

end;

registration

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

end;

registration

cluster non zero rational set ;
existence

proof end;

end;

registration

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

end;

theorem :: BORSUK_5:46

canceled;

theorem Th47: :: BORSUK_5:47

for a, b being real number st a < b holds
ex p1, p2 being rational number st
( a < p1 & p1 < p2 & p2 < b )

proof end;

Lm5: for s1, s3, s4, l being real number st s1 <= s3 & s1 < s4 & 0 < l & l < 1 holds
s1 < ((1 - l) * s3) + (l * s4)
by XREAL_1:179;

Lm6: for s1, s3, s4, l being real number st s3 < s1 & s4 <= s1 & 0 < l & l < 1 holds
((1 - l) * s3) + (l * s4) < s1
by XREAL_1:180;

theorem :: BORSUK_5:48

canceled;

theorem :: BORSUK_5:49

canceled;

theorem Th50: :: BORSUK_5:50

for a, b being real number st a < b holds
ex p being real irrational number st
( a < p & p < b )

proof end;

theorem Th51: :: BORSUK_5:51

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

proof end;

Lm7: for A being Subset of R^1
for a, b being real number st a < b & A = RAT a,b holds
( a in Cl A & b in Cl A )

proof end;

Lm8: for A being Subset of R^1
for a, b being real number st a < b & A = IRRAT a,b holds
( a in Cl A & b in Cl A )

proof end;

theorem Th52: :: BORSUK_5:52

for a, b, c being real number st a < b holds
( c in RAT a,b iff ( not c is irrational & a < c & c < b ) )

proof end;

theorem Th53: :: BORSUK_5:53

for a, b, c being real number st a < b holds
( c in IRRAT a,b iff ( c is irrational & a < c & c < b ) )

proof end;

theorem Th54: :: BORSUK_5:54

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

proof end;

theorem Th55: :: BORSUK_5:55

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

proof end;

theorem Th56: :: BORSUK_5:56

for T being connected TopSpace
for A being open closed Subset of T holds
( A = {} or A = [#] T )

proof end;

theorem Th57: :: BORSUK_5:57

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

proof end;

theorem Th58: :: BORSUK_5:58

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

proof end;

theorem Th59: :: BORSUK_5:59

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

proof end;

theorem :: BORSUK_5:60

for A being Subset of R^1
for a, b, c being real number st A = [.a,b.[ \/ ].b,c.] & a < b & b < c holds
Cl A = [.a,c.]

proof end;

theorem Th61: :: BORSUK_5:61

for A being Subset of R^1
for a being real number st A = {a} holds
Cl A = {a}

proof end;

theorem Th62: :: BORSUK_5:62

for A being Subset of REAL
for B being Subset of R^1 st A = B holds
( A is open iff B is open )

proof end;

Lm9: for a being real number holds ].a,+infty.[ is open
by FCONT_3:7;

Lm10: for a being real number holds ].-infty,a.] is closed
by FCONT_3:6;

Lm11: for a being real number holds ].-infty,a.[ is open
by FCONT_3:8;

Lm12: for a being real number holds [.a,+infty.[ is closed
by FCONT_3:5;

theorem Th63: :: BORSUK_5:63

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

proof end;

theorem Th64: :: BORSUK_5:64

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

proof end;

theorem Th65: :: BORSUK_5:65

for A being Subset of R^1
for a being real number st A = ].-infty,a.] holds
A is closed

proof end;

theorem Th66: :: BORSUK_5:66

for A being Subset of R^1
for a being real number st A = [.a,+infty.[ holds
A is closed

proof end;

theorem Th67: :: BORSUK_5:67

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

proof end;

theorem Th68: :: BORSUK_5:68

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

proof end;

Lm13: for a being real number holds ].a,+infty.[ c= [.a,+infty.[
by LIMFUNC1:10;

Lm14: for a being real number holds ].-infty,a.[ c= ].-infty,a.]
by LIMFUNC1:15;

registration

let a 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 :: BORSUK_5:69

canceled;

theorem :: BORSUK_5:70

canceled;

theorem Th71: :: BORSUK_5:71

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

proof end;

theorem :: BORSUK_5:72

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

proof end;

theorem :: BORSUK_5:73

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

proof end;

theorem Th74: :: BORSUK_5:74

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

proof end;

theorem Th75: :: BORSUK_5:75

for A being Subset of R^1
for a being real number st A = ].a,+infty.[ holds
Cl A = [.a,+infty.[

proof end;

theorem :: BORSUK_5:76

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

proof end;

theorem Th77: :: BORSUK_5:77

for A being Subset of R^1
for a being real number st A = ].-infty,a.[ holds
Cl A = ].-infty,a.]

proof end;

theorem :: BORSUK_5:78

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

proof end;

theorem Th79: :: BORSUK_5:79

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

proof end;

theorem :: BORSUK_5:80

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

proof end;

theorem Th81: :: BORSUK_5:81

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

proof end;

theorem :: BORSUK_5:82

for A being Subset of R^1
for a, b, c being real number st a < b & b < c & A = ((RAT a,b) \/ ].b,c.[) \/ ].c,+infty.[ holds
Cl A = [.a,+infty.[

proof end;

theorem :: BORSUK_5:83

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

theorem Th84: :: BORSUK_5:84

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

proof end;

Lm15: for a, b being real number st b <= a holds
RAT a,b = {}

proof end;

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

proof end;

theorem Th85: :: BORSUK_5:85

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

proof end;

theorem Th86: :: BORSUK_5:86

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

proof end;

theorem Th87: :: BORSUK_5:87

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

proof end;

theorem Th88: :: BORSUK_5:88

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

proof end;

theorem :: BORSUK_5:89

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

proof end;

theorem :: BORSUK_5:90

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

proof end;

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

proof end;

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

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

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

proof end;

theorem Th91: :: BORSUK_5:91

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

proof end;

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

proof end;

theorem :: 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 a, b being real number st a <= b holds
].-infty,b.[ \ {a} = ].-infty,a.[ \/ ].a,b.[

proof end;

theorem Th94: :: BORSUK_5:94

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

proof end;

theorem :: BORSUK_5:95

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

proof end;

theorem :: BORSUK_5:96

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

proof end;

theorem Th97: :: BORSUK_5:97

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

proof end;

theorem :: BORSUK_5:98

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

proof end;

theorem :: BORSUK_5:99

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

proof end;

theorem Th100: :: BORSUK_5:100

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

proof end;

theorem :: BORSUK_5:101

for A being Subset of R^1
for a, b, c, d being real number st a < b & b < c & A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT b,c)) \/ {c}) \/ {d} holds
Cl A = ].-infty,c.] \/ {d}

proof end;

theorem :: BORSUK_5:102

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

proof end;

theorem :: BORSUK_5:103

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

proof end;

theorem :: BORSUK_5:104

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

proof end;

theorem :: BORSUK_5:105

for TS being TopStruct
for A, B being Subset of TS st A <> B holds
A ` <> B `

proof end;

theorem :: BORSUK_5:106

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

proof end;

registration

cluster K384() -> arcwise_connected ;
coherence

proof end;

end;

theorem Th107: :: BORSUK_5:107

for X being compact Subset of R^1
for X' being Subset of REAL st X' = X holds
( X' is bounded_above & X' is bounded_below )

proof end;

theorem Th108: :: BORSUK_5:108

for X being compact Subset of R^1
for X' being Subset of REAL
for x being real number st x in X' & X' = X holds
( inf X' <= x & x <= sup X' )

proof end;

theorem Th109: :: BORSUK_5:109

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

proof end;

theorem Th110: :: BORSUK_5:110

for A being connected Subset of R^1
for a, b, c being real number st a <= b & b <= c & a in A & c in A holds
b in A

proof end;

theorem Th111: :: BORSUK_5:111

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

proof end;

theorem Th112: :: BORSUK_5:112

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

proof end;

theorem :: BORSUK_5:113

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

proof end;

definition

let TS be TopStruct ;
let F be Subset-Family of TS;
attr F is with_proper_subsets means :Def6: :: BORSUK_5:def 6
not the carrier of TS in F;

end;

:: deftheorem Def6 defines with_proper_subsets BORSUK_5:def 6 :

theorem :: BORSUK_5:114

for TS being TopStruct
for F, G being Subset-Family of TS st F is with_proper_subsets & G c= F holds
G is with_proper_subsets

proof end;

registration

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

proof end;

end;

theorem :: BORSUK_5:115

for TS being non empty TopStruct
for A, B being with_proper_subsets Subset-Family of TS holds A \/ B is with_proper_subsets

proof end;

registration

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

proof end;

end;