borsuk_4.miz

begin

 registration

 cluster -> non trivial for Simple_closed_curve;

 coherence

 proof

 let D be Simple_closed_curve;

 ex p1,p2 be Point of ( TOP-REAL 2) st p1 <> p2 & p1 in D & p2 in D by TOPREAL2: 5;

 hence thesis;

 end;

 end

 ::$Canceled

 theorem :: BORSUK_4:4



 Th1: for f,g be Function, a be set st f is one-to-one & g is one-to-one & (( dom f) /\ ( dom g)) = {a} & (( rng f) /\ ( rng g)) = {(f . a)} holds (f +* g) is one-to-one

 proof

 let f,g be Function, a be set;

 assume that

 A1: f is one-to-one and

 A2: g is one-to-one and

 A3: (( dom f) /\ ( dom g)) = {a} and

 A4: (( rng f) /\ ( rng g)) = {(f . a)};

 for x1,x2 be set st x1 in ( dom g) & x2 in (( dom f) \ ( dom g)) holds (g . x1) <> (f . x2)

 proof

 {a} c= ( dom g) by A3, XBOOLE_1: 17;

 then

 A5: a in ( dom g) by ZFMISC_1: 31;

 {a} c= ( dom f) by A3, XBOOLE_1: 17;

 then

 A6: a in ( dom f) by ZFMISC_1: 31;

 let x1,x2 be set;

 assume that

 A7: x1 in ( dom g) and

 A8: x2 in (( dom f) \ ( dom g));



 A9: (f . x2) in ( rng f) by A8, FUNCT_1: 3;

 assume

 A10: (g . x1) = (f . x2);

 (g . x1) in ( rng g) by A7, FUNCT_1: 3;

 then (f . x2) in (( rng f) /\ ( rng g)) by A9, A10, XBOOLE_0:def 4;

 then (f . x2) = (f . a) by A4, TARSKI:def 1;

 then x2 = a by A1, A8, A6, FUNCT_1:def 4;

 then ( dom g) meets (( dom f) \ ( dom g)) by A8, A5, XBOOLE_0: 3;

 hence thesis by XBOOLE_1: 79;

 end;

 hence thesis by A1, A2, TOPMETR2: 1;

 end;

 theorem :: BORSUK_4:5



 Th2: for f,g be Function, a be set st f is one-to-one & g is one-to-one & (( dom f) /\ ( dom g)) = {a} & (( rng f) /\ ( rng g)) = {(f . a)} & (f . a) = (g . a) holds ((f +* g) " ) = ((f " ) +* (g " ))

 proof

 let f,g be Function, a be set;

 assume that

 A1: f is one-to-one and

 A2: g is one-to-one and

 A3: (( dom f) /\ ( dom g)) = {a} and

 A4: (( rng f) /\ ( rng g)) = {(f . a)} and

 A5: (f . a) = (g . a);



 A6: ( dom (g " )) = ( rng g) by A2, FUNCT_1: 33;



 A7: ( dom (f " )) = ( rng f) by A1, FUNCT_1: 33;

 for x be object st x in (( dom (f " )) /\ ( dom (g " ))) holds ((f " ) . x) = ((g " ) . x)

 proof

 let x be object;

 {a} c= ( dom f) by A3, XBOOLE_1: 17;

 then

 A8: a in ( dom f) by ZFMISC_1: 31;

 assume

 A9: x in (( dom (f " )) /\ ( dom (g " )));

 then x = (f . a) by A4, A7, A6, TARSKI:def 1;

 then

 A10: a = ((f " ) . x) by A1, A8, FUNCT_1: 32;

 {a} c= ( dom g) by A3, XBOOLE_1: 17;

 then

 A11: a in ( dom g) by ZFMISC_1: 31;

 x = (g . a) by A4, A5, A7, A6, A9, TARSKI:def 1;

 hence thesis by A2, A11, A10, FUNCT_1: 32;

 end;

 then

 A12: (f " ) tolerates (g " );

 set gf = ((f " ) +* (g " )), F = (f +* g);

 for x be object st x in (( dom f) /\ ( dom g)) holds (f . x) = (g . x)

 proof

 let x be object;

 assume x in (( dom f) /\ ( dom g));

 then x = a by A3, TARSKI:def 1;

 hence thesis by A5;

 end;

 then

 A13: f tolerates g;

 ( dom gf) = (( dom (f " )) \/ ( dom (g " ))) by FUNCT_4:def 1

 .= (( rng f) \/ ( dom (g " ))) by A1, FUNCT_1: 33

 .= (( rng f) \/ ( rng g)) by A2, FUNCT_1: 33;

 then

 A14: ( dom gf) = ( rng F) by A13, FRECHET: 35;



 A15: ( dom F) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1;

 then

 A16: ( dom f) c= ( dom F) by XBOOLE_1: 7;



 A17: ( dom g) c= ( dom F) by A15, XBOOLE_1: 7;



 A18: ( rng F) = (( rng f) \/ ( rng g)) by A13, FRECHET: 35;



 A19: for y,x be object holds y in ( rng F) & x = (gf . y) iff x in ( dom F) & y = (F . x)

 proof

 let y,x be object;

 hereby

 assume that

 A20: y in ( rng F) and

 A21: x = (gf . y);

 per cases by A14, A20, FUNCT_4: 12;

 suppose

 A22: y in ( dom (f " ));

 then

 A23: y in ( rng f) by A1, FUNCT_1: 33;



 A24: x = ((f " ) . y) by A12, A21, A22, FUNCT_4: 15;

 then

 A25: y = (f . x) by A1, A23, FUNCT_1: 32;

 x in ( dom f) by A1, A23, A24, FUNCT_1: 32;

 hence x in ( dom F) & y = (F . x) by A13, A16, A25, FUNCT_4: 15;

 end;

 suppose

 A26: y in ( dom (g " ));

 then

 A27: x = ((g " ) . y) by A21, FUNCT_4: 13;



 A28: y in ( rng g) by A2, A26, FUNCT_1: 33;

 then

 A29: y = (g . x) by A2, A27, FUNCT_1: 32;

 x in ( dom g) by A2, A28, A27, FUNCT_1: 32;

 hence x in ( dom F) & y = (F . x) by A17, A29, FUNCT_4: 13;

 end;

 end;

 assume that

 A30: x in ( dom F) and

 A31: y = (F . x);

 per cases by A30, FUNCT_4: 12;

 suppose

 A32: x in ( dom f);

 then

 A33: y = (f . x) by A13, A31, FUNCT_4: 15;

 then

 A34: x = ((f " ) . y) by A1, A32, FUNCT_1: 32;

 ( rng F) = (( rng f) \/ ( rng g)) by A13, FRECHET: 35;

 then

 A35: ( rng f) c= ( rng F) by XBOOLE_1: 7;



 A36: y in ( rng f) by A32, A33, FUNCT_1: 3;

 then y in ( dom (f " )) by A1, FUNCT_1: 33;

 hence thesis by A12, A34, A36, A35, FUNCT_4: 15;

 end;

 suppose

 A37: x in ( dom g);

 then

 A38: y = (g . x) by A31, FUNCT_4: 13;

 then

 A39: x = ((g " ) . y) by A2, A37, FUNCT_1: 32;



 A40: ( rng g) c= ( rng F) by A18, XBOOLE_1: 7;



 A41: y in ( rng g) by A37, A38, FUNCT_1: 3;

 then y in ( dom (g " )) by A2, FUNCT_1: 33;

 hence thesis by A39, A41, A40, FUNCT_4: 13;

 end;

 end;

 F is one-to-one by A1, A2, A3, A4, Th1;

 hence thesis by A14, A19, FUNCT_1: 32;

 end;

 theorem :: BORSUK_4:6



 Th3: for n be Element of NAT , A be Subset of ( TOP-REAL n), p,q be Point of ( TOP-REAL n) st A is_an_arc_of (p,q) holds (A \ {p}) is non empty

 proof

 let n be Element of NAT , A be Subset of ( TOP-REAL n), p,q be Point of ( TOP-REAL n);

 assume A is_an_arc_of (p,q);

 then

 A1: (A \ {p, q}) <> {} by JORDAN6: 43;

 {p} c= {p, q} by ZFMISC_1: 7;

 hence thesis by A1, XBOOLE_1: 3, XBOOLE_1: 34;

 end;

 theorem :: BORSUK_4:7

 for s1,s3,s4,l be Real st s1 <= s3 & s1 < s4 & 0 <= l & l <= 1 holds s1 <= (((1 - l) * s3) + (l * s4))

 proof

 let s1,s3,s4,l be Real;

 assume that

 A1: s1 <= s3 and

 A2: s1 < s4 and

 A3: 0 <= l and

 A4: l <= 1;

 now

 per cases ;

 suppose l = 0 ;

 hence thesis by A1;

 end;

 suppose l = 1;

 hence thesis by A2;

 end;

 suppose

 A5: not (l = 0 or l = 1);

 then l < 1 by A4, XXREAL_0: 1;

 then (1 - l) > 0 by XREAL_1: 50;

 then

 A6: ((1 - l) * s1) <= ((1 - l) * s3) by A1, XREAL_1: 64;



 A7: (((1 - l) * s1) + (l * s1)) = (1 * s1);

 (l * s1) < (l * s4) by A2, A3, A5, XREAL_1: 68;

 hence thesis by A6, A7, XREAL_1: 8;

 end;

 end;

 hence thesis;

 end;

 theorem :: BORSUK_4:8



 Th5: for A be Subset of I[01] , a,b be Real st a < b & A = ].a, b.[ holds [.a, b.] c= the carrier of I[01]

 proof

 let A be Subset of I[01] , a,b be Real;

 assume

 A1: a < b;

 assume

 A2: A = ].a, b.[;

 then

 A3: b <= 1 by A1, BORSUK_1: 40, XXREAL_1: 51;

 0 <= a by A1, A2, BORSUK_1: 40, XXREAL_1: 51;

 hence thesis by A3, BORSUK_1: 40, XXREAL_1: 34;

 end;

 theorem :: BORSUK_4:9



 Th6: for A be Subset of I[01] , a,b be Real st a < b & A = ].a, b.] holds [.a, b.] c= the carrier of I[01]

 proof

 let A be Subset of I[01] , a,b be Real;

 assume

 A1: a < b;



 A2: ].a, b.[ c= ].a, b.] by XXREAL_1: 21;

 assume A = ].a, b.];

 then

 A3: ].a, b.[ c= [. 0 , 1.] by A2, BORSUK_1: 40, XBOOLE_1: 1;

 then

 A4: b <= 1 by A1, XXREAL_1: 51;

 0 <= a by A1, A3, XXREAL_1: 51;

 hence thesis by A4, BORSUK_1: 40, XXREAL_1: 34;

 end;

 theorem :: BORSUK_4:10



 Th7: for A be Subset of I[01] , a,b be Real st a < b & A = [.a, b.[ holds [.a, b.] c= the carrier of I[01]

 proof

 let A be Subset of I[01] , a,b be Real;

 assume

 A1: a < b;



 A2: ].a, b.[ c= [.a, b.[ by XXREAL_1: 22;

 assume A = [.a, b.[;

 then

 A3: ].a, b.[ c= [. 0 , 1.] by A2, BORSUK_1: 40, XBOOLE_1: 1;

 then

 A4: b <= 1 by A1, XXREAL_1: 51;

 0 <= a by A1, A3, XXREAL_1: 51;

 hence thesis by A4, BORSUK_1: 40, XXREAL_1: 34;

 end;

 theorem :: BORSUK_4:11



 Th8: for a,b be Real st a <> b holds ( Cl ].a, b.]) = [.a, b.]

 proof

 let a,b be Real;



 A1: ( Cl ].a, b.]) c= [.a, b.] by MEASURE6: 57, XXREAL_1: 23;



 A2: ( Cl ].a, b.[) c= ( Cl ].a, b.]) by MEASURE6: 62, XXREAL_1: 21;

 assume a <> b;

 then [.a, b.] c= ( Cl ].a, b.]) by A2, JORDAN5A: 26;

 hence thesis by A1, XBOOLE_0:def 10;

 end;

 theorem :: BORSUK_4:12



 Th9: for a,b be Real st a <> b holds ( Cl [.a, b.[) = [.a, b.]

 proof

 let a,b be Real;



 A1: ( Cl [.a, b.[) c= [.a, b.] by MEASURE6: 57, XXREAL_1: 24;



 A2: ( Cl ].a, b.[) c= ( Cl [.a, b.[) by MEASURE6: 62, XXREAL_1: 22;

 assume a <> b;

 then [.a, b.] c= ( Cl [.a, b.[) by A2, JORDAN5A: 26;

 hence thesis by A1, XBOOLE_0:def 10;

 end;

 theorem :: BORSUK_4:13

 for A be Subset of I[01] , a,b be Real st a < b & A = ].a, b.[ holds ( Cl A) = [.a, b.]

 proof

 let A be Subset of I[01] , a,b be Real;

 assume that

 A1: a < b and

 A2: A = ].a, b.[;

 reconsider A1 = ].a, b.[ as Subset of R^1 by TOPMETR: 17;



 A3: ( Cl ].a, b.[) = [.a, b.] by A1, JORDAN5A: 26;

 ( Cl A) = (( Cl A1) /\ ( [#] I[01] )) by A2, PRE_TOPC: 17

 .= ( [.a, b.] /\ ( [#] I[01] )) by A3, JORDAN5A: 24

 .= [.a, b.] by A1, A2, Th5, XBOOLE_1: 28;

 hence thesis;

 end;

 theorem :: BORSUK_4:14



 Th11: for A be Subset of I[01] , a,b be Real st a < b & A = ].a, b.] holds ( Cl A) = [.a, b.]

 proof

 let A be Subset of I[01] , a,b be Real;

 assume that

 A1: a < b and

 A2: A = ].a, b.];

 reconsider A1 = ].a, b.] as Subset of R^1 by TOPMETR: 17;



 A3: ( Cl ].a, b.]) = [.a, b.] by A1, Th8;

 ( Cl A) = (( Cl A1) /\ ( [#] I[01] )) by A2, PRE_TOPC: 17

 .= ( [.a, b.] /\ ( [#] I[01] )) by A3, JORDAN5A: 24

 .= [.a, b.] by A1, A2, Th6, XBOOLE_1: 28;

 hence thesis;

 end;

 theorem :: BORSUK_4:15



 Th12: for A be Subset of I[01] , a,b be Real st a < b & A = [.a, b.[ holds ( Cl A) = [.a, b.]

 proof

 let A be Subset of I[01] , a,b be Real;

 assume that

 A1: a < b and

 A2: A = [.a, b.[;

 reconsider A1 = [.a, b.[ as Subset of R^1 by TOPMETR: 17;



 A3: ( Cl [.a, b.[) = [.a, b.] by A1, Th9;

 ( Cl A) = (( Cl A1) /\ ( [#] I[01] )) by A2, PRE_TOPC: 17

 .= ( [.a, b.] /\ ( [#] I[01] )) by A3, JORDAN5A: 24

 .= [.a, b.] by A1, A2, Th7, XBOOLE_1: 28;

 hence thesis;

 end;

 theorem :: BORSUK_4:16



 Th13: for A be Subset of I[01] , a,b be Real st a <= b & A = [.a, b.] holds 0 <= a & b <= 1

 proof

 let A be Subset of I[01] , a,b be Real;

 assume that

 A1: a <= b and

 A2: A = [.a, b.];



 A3: b in A by A1, A2, XXREAL_1: 1;

 a in A by A1, A2, XXREAL_1: 1;

 hence thesis by A3, BORSUK_1: 43;

 end;

 theorem :: BORSUK_4:17



 Th14: for A,B be Subset of I[01] , a,b,c be Real st a < b & b < c & A = [.a, b.[ & B = ].b, c.] holds (A,B) are_separated

 proof

 let A,B be Subset of I[01] , a,b,c be Real;

 assume that

 A1: a < b and

 A2: b < c and

 A3: A = [.a, b.[ and

 A4: B = ].b, c.];

 ( Cl A) = [.a, b.] by A1, A3, Th12;

 hence ( Cl A) misses B by A4, XXREAL_1: 90;

 ( Cl B) = [.b, c.] by A2, A4, Th11;

 hence thesis by A3, XXREAL_1: 95;

 end;

 theorem :: BORSUK_4:18

 for p1,p2 be Point of I[01] holds [.p1, p2.] is Subset of I[01] by BORSUK_1: 40, XXREAL_2:def 12;

 theorem :: BORSUK_4:19



 Th16: for a,b be Point of I[01] holds ].a, b.[ is Subset of I[01]

 proof

 let a,b be Point of I[01] ;



 A1: [.a, b.] is Subset of I[01] by BORSUK_1: 40, XXREAL_2:def 12;

 ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

 hence thesis by A1, XBOOLE_1: 1;

 end;

 begin

 theorem :: BORSUK_4:20

 for p be Real holds {p} is non empty closed_interval Subset of REAL

 proof

 let p be Real;



 A1: {p} = [.p, p.] by XXREAL_1: 17;

 thus thesis by A1, MEASURE5: 14;

 end;

 theorem :: BORSUK_4:21



 Th18: for A be non empty connected Subset of I[01] , a,b,c be Point of I[01] st a <= b & b <= c & a in A & c in A holds b in A

 proof

 let A be non empty connected Subset of I[01] , a,b,c be Point of I[01] ;

 assume that

 A1: a <= b and

 A2: b <= c and

 A3: a in A and

 A4: c in A;

 per cases by A1, A2, A3, A4, XXREAL_0: 1;

 suppose a = b or b = c;

 hence thesis by A3, A4;

 end;

 suppose

 A5: a < b & b < c & a in A & c in A;



 A6: ].b, 1.] c= [.b, 1.] by XXREAL_1: 23;



 A7: [. 0 , b.[ c= [. 0 , b.] by XXREAL_1: 24;



 A8: 0 <= a by BORSUK_1: 43;



 A9: c <= 1 by BORSUK_1: 43;

 then

 A10: b < 1 by A5, XXREAL_0: 2;

 then

 A11: b in [. 0 , 1.] by A5, A8, XXREAL_1: 1;

 1 in [. 0 , 1.] by XXREAL_1: 1;

 then

 A12: [.b, 1.] c= [. 0 , 1.] by A11, XXREAL_2:def 12;

 0 in [. 0 , 1.] by XXREAL_1: 1;

 then [. 0 , b.] c= [. 0 , 1.] by A11, XXREAL_2:def 12;

 then

 reconsider B = [. 0 , b.[, C = ].b, 1.] as non empty Subset of I[01] by A5, A8, A9, A7, A6, A12, BORSUK_1: 40, XBOOLE_1: 1, XXREAL_1: 2, XXREAL_1: 3;

 assume not b in A;

 then A c= ( [. 0 , 1.] \ {b}) by BORSUK_1: 40, ZFMISC_1: 34;

 then

 A13: A c= ( [. 0 , b.[ \/ ].b, 1.]) by A5, A8, A10, XXREAL_1: 201;

 now

 per cases by A5, A8, A10, A13, Th14, CONNSP_1: 16;

 suppose A c= B;

 hence contradiction by A5, XXREAL_1: 3;

 end;

 suppose A c= C;

 hence contradiction by A5, XXREAL_1: 2;

 end;

 end;

 hence thesis;

 end;

 end;

 theorem :: BORSUK_4:22



 Th19: for A be non empty connected Subset of I[01] , a,b be Real st a in A & b in A holds [.a, b.] c= A

 proof

 let A be non empty connected Subset of I[01] , a,b be Real;

 assume that

 A1: a in A and

 A2: b in A;

 let x be object;

 assume x in [.a, b.];

 then x in { y where y be Real : a <= y & y <= b } by RCOMP_1:def 1;

 then

 consider z be Real such that

 A3: z = x and

 A4: a <= z and

 A5: z <= b;



 A6: 0 <= z by A1, A4, BORSUK_1: 43;

 b <= 1 by A2, BORSUK_1: 43;

 then z <= 1 by A5, XXREAL_0: 2;

 then

 reconsider z as Point of I[01] by A6, BORSUK_1: 43;

 z in A by A1, A2, A4, A5, Th18;

 hence thesis by A3;

 end;

 theorem :: BORSUK_4:23



 Th20: for a,b be Real, A be Subset of I[01] st A = [.a, b.] holds A is closed

 proof

 let a,b be Real, A be Subset of I[01] ;

 assume

 A1: A = [.a, b.];

 per cases ;

 suppose

 A2: a <= b;

 then

 A3: b <= 1 by A1, Th13;

 0 <= a by A1, A2, Th13;

 then

 A4: ( Closed-Interval-TSpace (a,b)) is closed SubSpace of ( Closed-Interval-TSpace ( 0 ,1)) by A2, A3, TREAL_1: 3;

 then

 reconsider BA = the carrier of ( Closed-Interval-TSpace (a,b)) as Subset of ( Closed-Interval-TSpace ( 0 ,1)) by BORSUK_1: 1;

 BA is closed by A4, BORSUK_1:def 11;

 hence thesis by A1, A2, TOPMETR: 18, TOPMETR: 20;

 end;

 suppose a > b;

 then A = ( {} I[01] ) by A1, XXREAL_1: 29;

 hence thesis;

 end;

 end;

 theorem :: BORSUK_4:24



 Th21: for p1,p2 be Point of I[01] st p1 <= p2 holds [.p1, p2.] is non empty compact connected Subset of I[01]

 proof

 let p1,p2 be Point of I[01] ;



 A1: p2 <= 1 by BORSUK_1: 43;

 set S = [.p1, p2.];

 reconsider S as Subset of I[01] by BORSUK_1: 40, XXREAL_2:def 12;

 assume

 A2: p1 <= p2;

 then

 A3: ( Closed-Interval-TSpace (p1,p2)) is connected by TREAL_1: 20;



 A4: S is closed by Th20;

 0 <= p1 by BORSUK_1: 43;

 then ( I[01] | S) = ( Closed-Interval-TSpace (p1,p2)) by A2, A1, TOPMETR: 24;

 hence thesis by A4, A3, COMPTS_1: 8, CONNSP_1:def 3;

 end;

 theorem :: BORSUK_4:25



 Th22: for X be Subset of I[01] , X9 be Subset of REAL st X9 = X holds X9 is bounded_above bounded_below

 proof

 let X be Subset of I[01] , X9 be Subset of REAL ;

 assume

 A1: X9 = X;

 then for r be ExtReal st r in X9 holds r <= 1 by BORSUK_1: 43;

 then 1 is UpperBound of X9 by XXREAL_2:def 1;

 hence X9 is bounded_above by XXREAL_2:def 10;

 for r be ExtReal st r in X9 holds 0 <= r by A1, BORSUK_1: 43;

 then 0 is LowerBound of X9 by XXREAL_2:def 2;

 hence thesis by XXREAL_2:def 9;

 end;

 theorem :: BORSUK_4:26



 Th23: for X be Subset of I[01] , X9 be Subset of REAL , x be Real st x in X9 & X9 = X holds ( lower_bound X9) <= x & x <= ( upper_bound X9)

 proof

 let X be Subset of I[01] , X9 be Subset of REAL , x be Real;

 assume that

 A1: x in X9 and

 A2: X9 = X;

 X9 is bounded_above bounded_below by A2, Th22;

 hence thesis by A1, SEQ_4:def 1, SEQ_4:def 2;

 end;



 Lm1: I[01] is closed SubSpace of R^1 by TOPMETR: 20, TREAL_1: 2;

 theorem :: BORSUK_4:27



 Th24: for A be Subset of REAL , B be Subset of I[01] st A = B holds A is closed iff B is closed

 proof

 reconsider Z = the carrier of I[01] as Subset of R^1 by BORSUK_1: 1;

 let A be Subset of REAL , B be Subset of I[01] ;

 assume

 A1: A = B;

 the carrier of I[01] c= the carrier of R^1 by BORSUK_1: 1;

 then

 reconsider C = A as Subset of R^1 by A1, XBOOLE_1: 1;

 hereby

 assume A is closed;

 then

 A2: C is closed by JORDAN5A: 23;

 (C /\ ( [#] I[01] )) = B by A1, XBOOLE_1: 28;

 hence B is closed by A2, PRE_TOPC: 13;

 end;

 assume

 A3: B is closed;

 Z is closed by Lm1, BORSUK_1:def 11;

 then B is closed iff C is closed by A1, TSEP_1: 8;

 hence thesis by A3, JORDAN5A: 23;

 end;

 theorem :: BORSUK_4:28



 Th25: for C be non empty closed_interval Subset of REAL holds ( lower_bound C) <= ( upper_bound C)

 proof

 let C be non empty closed_interval Subset of REAL ;

 set c = the Element of C;



 A1: c <= ( upper_bound C) by INTEGRA2: 1;

 ( lower_bound C) <= c by INTEGRA2: 1;

 hence thesis by A1, XXREAL_0: 2;

 end;

 theorem :: BORSUK_4:29



 Th26: for C be non empty compact connected Subset of I[01] , C9 be Subset of REAL st C = C9 & [.( lower_bound C9), ( upper_bound C9).] c= C9 holds [.( lower_bound C9), ( upper_bound C9).] = C9

 proof

 let C be non empty compact connected Subset of I[01] , C9 be Subset of REAL ;

 assume that

 A1: C = C9 and

 A2: [.( lower_bound C9), ( upper_bound C9).] c= C9;

 assume [.( lower_bound C9), ( upper_bound C9).] <> C9;

 then not C9 c= [.( lower_bound C9), ( upper_bound C9).] by A2, XBOOLE_0:def 10;

 then

 consider c be object such that

 A3: c in C9 and

 A4: not c in [.( lower_bound C9), ( upper_bound C9).];

 reconsider c as Real by A3;



 A5: c <= ( upper_bound C9) by A1, A3, Th23;

 ( lower_bound C9) <= c by A1, A3, Th23;

 hence thesis by A4, A5, XXREAL_1: 1;

 end;

 theorem :: BORSUK_4:30



 Th27: for C be non empty compact connected Subset of I[01] holds C is non empty closed_interval Subset of REAL

 proof

 let C be non empty compact connected Subset of I[01] ;

 reconsider C9 = C as Subset of REAL by BORSUK_1: 40, XBOOLE_1: 1;

 C9 is bounded_below bounded_above by Th22;

 then

 A1: ( lower_bound C9) <= ( upper_bound C9) by SEQ_4: 11;



 A2: C9 is closed by Th24;

 then

 A3: ( upper_bound C9) in C9 by Th22, RCOMP_1: 12;

 ( lower_bound C9) in C9 by A2, Th22, RCOMP_1: 13;

 then [.( lower_bound C9), ( upper_bound C9).] = C9 by A3, Th19, Th26;

 hence thesis by A1, MEASURE5: 14;

 end;

 theorem :: BORSUK_4:31



 Th28: for C be non empty compact connected Subset of I[01] holds ex p1,p2 be Point of I[01] st p1 <= p2 & C = [.p1, p2.]

 proof

 let C be non empty compact connected Subset of I[01] ;

 reconsider C9 = C as non empty closed_interval Subset of REAL by Th27;



 A1: C9 = [.( lower_bound C9), ( upper_bound C9).] by INTEGRA1: 4;



 A2: ( lower_bound C9) <= ( upper_bound C9) by Th25;

 then

 A3: ( upper_bound C9) in C by A1, XXREAL_1: 1;

 ( lower_bound C9) in C by A1, A2, XXREAL_1: 1;

 then

 reconsider p1 = ( lower_bound C9), p2 = ( upper_bound C9) as Point of I[01] by A3;

 take p1, p2;

 thus p1 <= p2 by Th25;

 thus thesis by INTEGRA1: 4;

 end;

 begin

 definition

 :: BORSUK_4:def1

 func I(01) -> strict SubSpace of I[01] means

 : Def1: the carrier of it = ]. 0 , 1.[;

 existence

 proof

 reconsider E = ]. 0 , 1.[ as Subset of I[01] by BORSUK_1: 40, XXREAL_1: 25;

 take ( I[01] | E);

 thus thesis by PRE_TOPC: 8;

 end;

 uniqueness by TSEP_1: 5;

 end

 registration

 cluster I(01) -> non empty;

 coherence

 proof

 the carrier of I(01) = ]. 0 , 1.[ by Def1;

 hence the carrier of I(01) is non empty by XXREAL_1: 33;

 end;

 end

 theorem :: BORSUK_4:32

 for A be Subset of I[01] st A = the carrier of I(01) holds I(01) = ( I[01] | A) by PRE_TOPC: 8, TSEP_1: 5;

 theorem :: BORSUK_4:33



 Th30: the carrier of I(01) = (the carrier of I[01] \ { 0 , 1})

 proof



 A1: [. 0 , 1.] = ( ]. 0 , 1.[ \/ { 0 , 1}) by XXREAL_1: 128;

 the carrier of I(01) = ]. 0 , 1.[ by Def1;

 hence thesis by A1, BORSUK_1: 40, XBOOLE_1: 88, XXREAL_1: 86;

 end;

 registration

 cluster I(01) -> open;

 coherence by Th30, JORDAN6: 34, TSEP_1:def 1;

 end

 theorem :: BORSUK_4:34

 I(01) is open;

 theorem :: BORSUK_4:35



 Th32: for r be Real holds r in the carrier of I(01) iff 0 < r & r < 1

 proof

 let r be Real;

 hereby

 assume r in the carrier of I(01) ;

 then r in ]. 0 , 1.[ by Def1;

 hence 0 < r & r < 1 by XXREAL_1: 4;

 end;

 assume that

 A1: 0 < r and

 A2: r < 1;

 r in ]. 0 , 1.[ by A1, A2, XXREAL_1: 4;

 hence thesis by Def1;

 end;

 theorem :: BORSUK_4:36



 Th33: for a,b be Point of I[01] st a 1 holds ].a, b.] is non empty Subset of I(01)

 proof

 let a,b be Point of I[01] ;

 assume that

 A1: a 1;

 b <= 1 by BORSUK_1: 43;

 then

 A3: b < 1 by A2, XXREAL_0: 1;

 ].a, b.] c= the carrier of I(01)

 proof

 let x be object;

 assume x in ].a, b.];

 then x in { r where r be Real : a < r & r <= b } by RCOMP_1:def 8;

 then

 consider r be Real such that

 A4: x = r and

 A5: a < r and

 A6: r <= b;



 A7: 0 < r by A5, BORSUK_1: 43;

 r < 1 by A3, A6, XXREAL_0: 2;

 hence thesis by A4, A7, Th32;

 end;

 hence thesis by A1, XXREAL_1: 2;

 end;

 theorem :: BORSUK_4:37



 Th34: for a,b be Point of I[01] st a 0 holds [.a, b.[ is non empty Subset of I(01)

 proof

 let a,b be Point of I[01] ;

 assume that

 A1: a 0 ;



 A3: b <= 1 by BORSUK_1: 43;

 [.a, b.[ c= the carrier of I(01)

 proof

 let x be object;

 assume x in [.a, b.[;

 then x in { r where r be Real : a <= r & r < b } by RCOMP_1:def 7;

 then

 consider r be Real such that

 A4: x = r and

 A5: a <= r and

 A6: r < b;



 A7: r < 1 by A3, A6, XXREAL_0: 2;

 0 < r by A2, A5, BORSUK_1: 43;

 hence thesis by A4, A7, Th32;

 end;

 hence thesis by A1, XXREAL_1: 3;

 end;

 theorem :: BORSUK_4:38

 for D be Simple_closed_curve holds ((( TOP-REAL 2) | R^2-unit_square ),(( TOP-REAL 2) | D)) are_homeomorphic

 proof

 let D be Simple_closed_curve;

 ex f be Function of (( TOP-REAL 2) | R^2-unit_square ), (( TOP-REAL 2) | D) st f is being_homeomorphism by TOPREAL2:def 1;

 hence thesis by T_0TOPSP:def 1;

 end;

 theorem :: BORSUK_4:39

 for n be Element of NAT , D be non empty Subset of ( TOP-REAL n), p1,p2 be Point of ( TOP-REAL n) st D is_an_arc_of (p1,p2) holds ( I(01) ,(( TOP-REAL n) | (D \ {p1, p2}))) are_homeomorphic

 proof

 reconsider K0 = the carrier of I(01) as Subset of I[01] by BORSUK_1: 1;

 let n be Element of NAT , D be non empty Subset of ( TOP-REAL n), p1,p2 be Point of ( TOP-REAL n);

 assume

 A1: D is_an_arc_of (p1,p2);

 then

 consider f be Function of I[01] , (( TOP-REAL n) | D) such that

 A2: f is being_homeomorphism and

 A3: (f . 0 ) = p1 and

 A4: (f . 1) = p2 by TOPREAL1:def 1;



 A5: ( rng f) = ( [#] (( TOP-REAL n) | D)) by A2, TOPS_2:def 5

 .= D by PRE_TOPC: 8;



 A6: ( dom f) = the carrier of I[01] by FUNCT_2:def 1;

 then

 A7: 0 in ( dom f) by BORSUK_1: 43;



 A8: 1 in ( dom f) by A6, BORSUK_1: 43;



 A9: f is continuous one-to-one by A2, TOPS_2:def 5;



 then

 A10: (f .: the carrier of I(01) ) = ((f .: the carrier of I[01] ) \ (f .: { 0 , 1})) by Th30, FUNCT_1: 64

 .= (D \ (f .: { 0 , 1})) by A6, A5, RELAT_1: 113

 .= (D \ {p1, p2}) by A3, A4, A7, A8, FUNCT_1: 60;



 A11: (D \ {p1, p2}) c= D by XBOOLE_1: 36;

 then

 reconsider D0 = (D \ {p1, p2}) as Subset of (( TOP-REAL n) | D) by PRE_TOPC: 8;

 reconsider D1 = (D \ {p1, p2}) as non empty Subset of ( TOP-REAL n) by A1, JORDAN6: 43;



 A12: (( TOP-REAL n) | D1) = ((( TOP-REAL n) | D) | D0) by GOBOARD9: 2;

 set g = ((f " ) | D1);



 A13: D1 = the carrier of (( TOP-REAL n) | D1) by PRE_TOPC: 8;

 D1 c= the carrier of (( TOP-REAL n) | D) by A11, PRE_TOPC: 8;

 then

 reconsider ff = g as Function of (( TOP-REAL n) | D1), I[01] by A13, FUNCT_2: 32;

 (f " ) is continuous by A2, TOPS_2:def 5;

 then

 A14: ff is continuous by A12, TOPMETR: 7;

 set fD = (f | the carrier of I(01) );



 A15: I(01) = ( I[01] | K0) by PRE_TOPC: 8, TSEP_1: 5;

 then

 reconsider fD1 = fD as Function of ( I[01] | K0), (( TOP-REAL n) | D) by FUNCT_2: 32;



 A16: ( dom fD) = the carrier of I(01) by A6, BORSUK_1: 1, RELAT_1: 62;

 ( rng f) = ( [#] (( TOP-REAL n) | D)) by A2, TOPS_2:def 5;

 then f is onto by FUNCT_2:def 3;

 then

 A17: (f " ) = (f qua Function " ) by A9, TOPS_2:def 4;



 A18: ( rng fD) = (f .: the carrier of I(01) ) by RELAT_1: 115;

 then

 A19: ( rng fD) = the carrier of (( TOP-REAL n) | (D \ {p1, p2})) by A10, PRE_TOPC: 8;

 then

 reconsider fD as Function of I(01) , (( TOP-REAL n) | (D \ {p1, p2})) by A16, FUNCT_2: 1;



 A20: ( dom fD) = ( [#] I(01) ) by A6, BORSUK_1: 1, RELAT_1: 62;



 A21: fD is onto by A19, FUNCT_2:def 3;

 f is one-to-one by A2, TOPS_2:def 5;

 then

 A22: fD is one-to-one by FUNCT_1: 52;

 then (fD " ) = (fD qua Function " ) by A21, TOPS_2:def 4;

 then

 A23: (fD " ) is continuous by A9, A10, A15, A14, A17, RFUNCT_2: 17, TOPMETR: 6;

 fD1 is continuous by A9, TOPMETR: 7;

 then

 A24: fD is continuous by A15, A12, TOPMETR: 6;

 ( rng fD) = ( [#] (( TOP-REAL n) | (D \ {p1, p2}))) by A10, A18, PRE_TOPC: 8;

 then fD is being_homeomorphism by A20, A22, A24, A23, TOPS_2:def 5;

 hence thesis by T_0TOPSP:def 1;

 end;

 theorem :: BORSUK_4:40



 Th37: for n be Element of NAT , D be Subset of ( TOP-REAL n), p1,p2 be Point of ( TOP-REAL n) st D is_an_arc_of (p1,p2) holds ( I[01] ,(( TOP-REAL n) | D)) are_homeomorphic

 proof

 let n be Element of NAT , D be Subset of ( TOP-REAL n), p1,p2 be Point of ( TOP-REAL n);

 assume D is_an_arc_of (p1,p2);

 then ex f be Function of I[01] , (( TOP-REAL n) | D) st f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = p2 by TOPREAL1:def 1;

 hence thesis by T_0TOPSP:def 1;

 end;

 theorem :: BORSUK_4:41

 for n be Element of NAT , p1,p2 be Point of ( TOP-REAL n) st p1 <> p2 holds ( I[01] ,(( TOP-REAL n) | ( LSeg (p1,p2)))) are_homeomorphic by Th37, TOPREAL1: 9;

 theorem :: BORSUK_4:42



 Th39: for E be Subset of I(01) st (ex p1,p2 be Point of I[01] st p1 < p2 & E = [.p1, p2.]) holds ( I[01] ,( I(01) | E)) are_homeomorphic

 proof

 let E be Subset of I(01) ;

 given p1,p2 be Point of I[01] such that

 A1: p1 < p2 and

 A2: E = [.p1, p2.];



 A3: p2 <= 1 by BORSUK_1: 43;

 0 <= p1 by BORSUK_1: 43;

 then

 reconsider S = ( Closed-Interval-TSpace (p1,p2)) as SubSpace of I[01] by A1, A3, TOPMETR: 20, TREAL_1: 3;

 reconsider T = ( I(01) | E) as SubSpace of I[01] by TSEP_1: 7;

 the carrier of S = E by A1, A2, TOPMETR: 18;

 then

 A4: S = T by PRE_TOPC: 8, TSEP_1: 5;

 set f = ( L[01] (( (#) (p1,p2)),((p1,p2) (#) )));

 f is being_homeomorphism by A1, TREAL_1: 17;

 hence thesis by A4, TOPMETR: 20, T_0TOPSP:def 1;

 end;

 theorem :: BORSUK_4:43



 Th40: for n be Element of NAT , A be Subset of ( TOP-REAL n), p,q be Point of ( TOP-REAL n), a,b be Point of I[01] st A is_an_arc_of (p,q) & a < b holds ex E be non empty Subset of I[01] , f be Function of ( I[01] | E), (( TOP-REAL n) | A) st E = [.a, b.] & f is being_homeomorphism & (f . a) = p & (f . b) = q

 proof



 A1: 0 = ( (#) ( 0 ,1)) by TREAL_1:def 1;

 let n be Element of NAT , A be Subset of ( TOP-REAL n), p,q be Point of ( TOP-REAL n), a,b be Point of I[01] ;

 assume that

 A2: A is_an_arc_of (p,q) and

 A3: a < b;

 reconsider E = [.a, b.] as non empty Subset of I[01] by A3, Th21;



 A4: b <= 1 by BORSUK_1: 43;

 0 <= a by BORSUK_1: 43;

 then

 A5: ( I[01] | E) = ( Closed-Interval-TSpace (a,b)) by A3, A4, TOPMETR: 24;

 then

 reconsider e = ( P[01] (a,b,( (#) ( 0 ,1)),(( 0 ,1) (#) ))) as Function of ( I[01] | E), I[01] by TOPMETR: 20;

 take E;



 A6: a = ( (#) (a,b)) by A3, TREAL_1:def 1;

 reconsider B = A as non empty Subset of ( TOP-REAL n) by A2, TOPREAL1: 1;

 consider f be Function of I[01] , (( TOP-REAL n) | B) such that

 A7: f is being_homeomorphism and

 A8: (f . 0 ) = p and

 A9: (f . 1) = q by A2, TOPREAL1:def 1;

 set g = (f * e);

 reconsider g as Function of ( I[01] | E), (( TOP-REAL n) | A);

 take g;

 thus E = [.a, b.];

 e is being_homeomorphism by A3, A5, TOPMETR: 20, TREAL_1: 17;

 hence g is being_homeomorphism by A7, TOPS_2: 57;

 a in E by A3, XXREAL_1: 1;

 then a in the carrier of ( I[01] | E) by PRE_TOPC: 8;



 hence (g . a) = (f . (e . a)) by FUNCT_2: 15

 .= p by A3, A8, A1, A6, TREAL_1: 13;



 A10: 1 = (( 0 ,1) (#) ) by TREAL_1:def 2;



 A11: b = ((a,b) (#) ) by A3, TREAL_1:def 2;

 b in E by A3, XXREAL_1: 1;

 then b in the carrier of ( I[01] | E) by PRE_TOPC: 8;



 hence (g . b) = (f . (e . b)) by FUNCT_2: 15

 .= q by A3, A9, A10, A11, TREAL_1: 13;

 end;

 theorem :: BORSUK_4:44



 Th41: for A be TopSpace, B be non empty TopSpace, f be Function of A, B, C be TopSpace, X be Subset of A st f is continuous & C is SubSpace of B holds for h be Function of (A | X), C st h = (f | X) holds h is continuous

 proof

 let A be TopSpace, B be non empty TopSpace;

 let f be Function of A, B;

 let C be TopSpace, X be Subset of A;

 assume that

 A1: f is continuous and

 A2: C is SubSpace of B;

 the carrier of (A | X) = X by PRE_TOPC: 8;

 then

 reconsider g = (f | X) as Function of (A | X), B by FUNCT_2: 32;

 let h be Function of (A | X), C;

 assume

 A3: h = (f | X);

 g is continuous by A1, TOPMETR: 7;

 hence thesis by A2, A3, PRE_TOPC: 27;

 end;

 theorem :: BORSUK_4:45



 Th42: for X be Subset of I[01] , a,b be Point of I[01] st X = ].a, b.[ holds X is open

 proof

 let X be Subset of I[01] , a,b be Point of I[01] ;



 A1: 0 <= a by BORSUK_1: 43;

 1 in the carrier of I[01] by BORSUK_1: 43;

 then

 reconsider B = [.b, 1.] as Subset of I[01] by BORSUK_1: 40, XXREAL_2:def 12;

 0 in the carrier of I[01] by BORSUK_1: 43;

 then

 reconsider A = [. 0 , a.] as Subset of I[01] by BORSUK_1: 40, XXREAL_2:def 12;



 A2: b <= 1 by BORSUK_1: 43;



 A3: B is closed by Th20;



 A4: A is closed by Th20;

 assume X = ].a, b.[;

 then X = ((A \/ B) ` ) by A1, A2, BORSUK_1: 40, XXREAL_1: 200;

 hence thesis by A4, A3;

 end;

 theorem :: BORSUK_4:46



 Th43: for X be Subset of I(01) , a,b be Point of I[01] st X = ].a, b.[ holds X is open

 proof

 let X be Subset of I(01) , a,b be Point of I[01] ;

 assume

 A1: X = ].a, b.[;

 then

 reconsider X9 = X as Subset of I[01] by Th16;

 X9 is open by A1, Th42;

 hence thesis by TSEP_1: 17;

 end;

 theorem :: BORSUK_4:47



 Th44: for X be Subset of I(01) , a be Point of I[01] st X = ]. 0 , a.] holds X is closed

 proof

 let X be Subset of I(01) , a be Point of I[01] ;

 assume

 A1: X = ]. 0 , a.];

 per cases ;

 suppose

 A2: 0 < a;

 ( [#] I(01) ) = ]. 0 , 1.[ by Def1;

 then

 A3: (( [#] I(01) ) \ X) = ].a, 1.[ by A1, A2, XXREAL_1: 187;

 1 in the carrier of I[01] by BORSUK_1: 43;

 then (( [#] I(01) ) \ X) is open by A3, Th43;

 hence thesis by PRE_TOPC:def 3;

 end;

 suppose 0 >= a;

 then X = ( {} I(01) ) by A1, XXREAL_1: 26;

 hence thesis;

 end;

 end;

 theorem :: BORSUK_4:48



 Th45: for X be Subset of I(01) , a be Point of I[01] st X = [.a, 1.[ holds X is closed

 proof



 A1: 0 in the carrier of I[01] by BORSUK_1: 43;

 let X be Subset of I(01) , a be Point of I[01] ;

 assume

 A2: X = [.a, 1.[;

 per cases ;

 suppose

 A3: X is non empty;



 A4: a <= 1 by BORSUK_1: 43;

 a <> 1 by A2, A3, XXREAL_1: 18;

 then

 A5: a < 1 by A4, XXREAL_0: 1;

 ( [#] I(01) ) = ]. 0 , 1.[ by Def1;

 then (( [#] I(01) ) \ X) = ]. 0 , a.[ by A2, A5, XXREAL_1: 195;

 then (( [#] I(01) ) \ X) is open by A1, Th43;

 hence thesis by PRE_TOPC:def 3;

 end;

 suppose X is empty;

 hence thesis;

 end;

 end;

 theorem :: BORSUK_4:49



 Th46: for n be Element of NAT , A be Subset of ( TOP-REAL n), p,q be Point of ( TOP-REAL n), a,b be Point of I[01] st A is_an_arc_of (p,q) & a 1 holds ex E be non empty Subset of I(01) , f be Function of ( I(01) | E), (( TOP-REAL n) | (A \ {p})) st E = ].a, b.] & f is being_homeomorphism & (f . b) = q

 proof

 let n be Element of NAT , A be Subset of ( TOP-REAL n), p,q be Point of ( TOP-REAL n), a,b be Point of I[01] ;

 assume that

 A1: A is_an_arc_of (p,q) and

 A2: a 1;

 reconsider B = A as non empty Subset of ( TOP-REAL n) by A1, TOPREAL1: 1;

 consider F be non empty Subset of I[01] , s be Function of ( I[01] | F), (( TOP-REAL n) | B) such that

 A4: F = [.a, b.] and

 A5: s is being_homeomorphism and

 A6: (s . a) = p and

 A7: (s . b) = q by A1, A2, Th40;



 A8: ( dom s) = ( [#] ( I[01] | F)) by A5, TOPS_2:def 5

 .= F by PRE_TOPC:def 5;

 then

 A9: a in ( dom s) by A2, A4, XXREAL_1: 1;

 reconsider E = ].a, b.] as non empty Subset of I(01) by A2, A3, Th33;

 set X = E;



 A10: ( I(01) | X) is SubSpace of I[01] by TSEP_1: 7;

 set sX = (s | E);



 A11: s is continuous one-to-one by A5, TOPS_2:def 5;



 A12: (s " ) is continuous by A5, TOPS_2:def 5;



 A13: the carrier of (( TOP-REAL n) | A) = A by PRE_TOPC: 8;

 then

 reconsider Ap = (A \ {p}) as Subset of (( TOP-REAL n) | A) by XBOOLE_1: 36;

 the carrier of (( TOP-REAL n) | (A \ {p})) = (A \ {p}) by PRE_TOPC: 8;

 then the carrier of (( TOP-REAL n) | (A \ {p})) c= the carrier of (( TOP-REAL n) | A) by A13, XBOOLE_1: 36;

 then

 A14: (( TOP-REAL n) | (A \ {p})) is SubSpace of (( TOP-REAL n) | A) by TSEP_1: 4;



 A15: E c= F by A4, XXREAL_1: 23;

 then

 reconsider X9 = E as Subset of ( I[01] | F) by PRE_TOPC: 8;



 A16: (( I[01] | F) | X9) is SubSpace of I[01] by TSEP_1: 7;

 the carrier of ( I(01) | E) = E by PRE_TOPC: 8;

 then the carrier of ( I(01) | X) c= the carrier of ( I[01] | F) by A15, PRE_TOPC: 8;

 then

 A17: ( I(01) | X) is SubSpace of ( I[01] | F) by A10, TSEP_1: 4;



 A18: ((( TOP-REAL n) | A) | Ap) = (( TOP-REAL n) | (A \ {p})) by PRE_TOPC: 7, XBOOLE_1: 36;



 A19: ( dom sX) = X by A4, A8, RELAT_1: 62, XXREAL_1: 23

 .= ( [#] ( I(01) | X)) by PRE_TOPC:def 5;



 A20: ( rng s) = ( [#] (( TOP-REAL n) | A)) by A5, TOPS_2:def 5;

 then

 A21: ( rng s) = A by PRE_TOPC:def 5;

 X = (F \ {a}) by A2, A4, XXREAL_1: 134;



 then

 A22: (s .: X) = ((s .: F) \ ( Im (s,a))) by A11, FUNCT_1: 64

 .= ((s .: F) \ {(s . a)}) by A9, FUNCT_1: 59

 .= (( rng s) \ {p}) by A6, A8, RELAT_1: 113

 .= ( [#] (( TOP-REAL n) | (A \ {p}))) by A21, PRE_TOPC:def 5;

 then

 A23: ( [#] (( TOP-REAL n) | (A \ {p}))) = ( rng sX) by RELAT_1: 115;

 ( rng (s | E)) = the carrier of (( TOP-REAL n) | (A \ {p})) by A22, RELAT_1: 115;

 then

 reconsider sX as Function of ( I(01) | E), (( TOP-REAL n) | (A \ {p})) by A19, FUNCT_2: 1;



 A24: s is onto by A20, FUNCT_2:def 3;



 A25: sX is onto by A23, FUNCT_2:def 3;

 b in X by A2, XXREAL_1: 2;

 then

 A26: (sX . b) = q by A7, FUNCT_1: 49;

 the carrier of ( I(01) | X) = X by PRE_TOPC: 8;

 then ( I(01) | X) = (( I[01] | F) | X9) by A10, A16, PRE_TOPC: 8, TSEP_1: 5;

 then

 A27: sX is continuous by A11, A14, Th41;



 A28: sX is one-to-one by A11, FUNCT_1: 52;



 then (sX " ) = (sX qua Function " ) by A25, TOPS_2:def 4

 .= ((s qua Function " ) | (s .: X)) by A11, RFUNCT_2: 17

 .= ((s " ) | ( [#] (( TOP-REAL n) | (A \ {p})))) by A24, A11, A22, TOPS_2:def 4

 .= ((s " ) | Ap) by PRE_TOPC:def 5;

 then (sX " ) is continuous by A12, A17, A18, Th41;

 then sX is being_homeomorphism by A23, A19, A27, A28, TOPS_2:def 5;

 hence thesis by A26;

 end;

 theorem :: BORSUK_4:50



 Th47: for n be Element of NAT , A be Subset of ( TOP-REAL n), p,q be Point of ( TOP-REAL n), a,b be Point of I[01] st A is_an_arc_of (p,q) & a 0 holds ex E be non empty Subset of I(01) , f be Function of ( I(01) | E), (( TOP-REAL n) | (A \ {q})) st E = [.a, b.[ & f is being_homeomorphism & (f . a) = p

 proof

 let n be Element of NAT , A be Subset of ( TOP-REAL n), p,q be Point of ( TOP-REAL n), a,b be Point of I[01] ;

 assume that

 A1: A is_an_arc_of (p,q) and

 A2: a 0 ;

 reconsider B = A as non empty Subset of ( TOP-REAL n) by A1, TOPREAL1: 1;

 consider F be non empty Subset of I[01] , s be Function of ( I[01] | F), (( TOP-REAL n) | B) such that

 A4: F = [.a, b.] and

 A5: s is being_homeomorphism and

 A6: (s . a) = p and

 A7: (s . b) = q by A1, A2, Th40;



 A8: ( dom s) = ( [#] ( I[01] | F)) by A5, TOPS_2:def 5

 .= F by PRE_TOPC:def 5;

 then

 A9: b in ( dom s) by A2, A4, XXREAL_1: 1;

 reconsider E = [.a, b.[ as non empty Subset of I(01) by A2, A3, Th34;

 set X = E;



 A10: ( I(01) | X) is SubSpace of I[01] by TSEP_1: 7;

 set sX = (s | E);



 A11: s is continuous one-to-one by A5, TOPS_2:def 5;



 A12: (s " ) is continuous by A5, TOPS_2:def 5;



 A13: the carrier of (( TOP-REAL n) | A) = A by PRE_TOPC: 8;

 then

 reconsider Ap = (A \ {q}) as Subset of (( TOP-REAL n) | A) by XBOOLE_1: 36;

 the carrier of (( TOP-REAL n) | (A \ {q})) = (A \ {q}) by PRE_TOPC: 8;

 then the carrier of (( TOP-REAL n) | (A \ {q})) c= the carrier of (( TOP-REAL n) | A) by A13, XBOOLE_1: 36;

 then

 A14: (( TOP-REAL n) | (A \ {q})) is SubSpace of (( TOP-REAL n) | A) by TSEP_1: 4;



 A15: E c= F by A4, XXREAL_1: 24;

 then

 reconsider X9 = E as Subset of ( I[01] | F) by PRE_TOPC: 8;



 A16: (( I[01] | F) | X9) is SubSpace of I[01] by TSEP_1: 7;

 the carrier of ( I(01) | E) = E by PRE_TOPC: 8;

 then the carrier of ( I(01) | X) c= the carrier of ( I[01] | F) by A15, PRE_TOPC: 8;

 then

 A17: ( I(01) | X) is SubSpace of ( I[01] | F) by A10, TSEP_1: 4;



 A18: ((( TOP-REAL n) | A) | Ap) = (( TOP-REAL n) | (A \ {q})) by PRE_TOPC: 7, XBOOLE_1: 36;



 A19: ( dom sX) = X by A4, A8, RELAT_1: 62, XXREAL_1: 24

 .= ( [#] ( I(01) | X)) by PRE_TOPC:def 5;



 A20: ( rng s) = ( [#] (( TOP-REAL n) | A)) by A5, TOPS_2:def 5;

 then

 A21: ( rng s) = A by PRE_TOPC:def 5;

 X = (F \ {b}) by A2, A4, XXREAL_1: 135;



 then

 A22: (s .: X) = ((s .: F) \ ( Im (s,b))) by A11, FUNCT_1: 64

 .= ((s .: F) \ {(s . b)}) by A9, FUNCT_1: 59

 .= (( rng s) \ {q}) by A7, A8, RELAT_1: 113

 .= ( [#] (( TOP-REAL n) | (A \ {q}))) by A21, PRE_TOPC:def 5;

 then

 A23: ( [#] (( TOP-REAL n) | (A \ {q}))) = ( rng sX) by RELAT_1: 115;

 ( rng (s | E)) = the carrier of (( TOP-REAL n) | (A \ {q})) by A22, RELAT_1: 115;

 then

 reconsider sX as Function of ( I(01) | E), (( TOP-REAL n) | (A \ {q})) by A19, FUNCT_2: 1;



 A24: sX is onto by A23, FUNCT_2:def 3;



 A25: s is onto by A20, FUNCT_2:def 3;

 a in X by A2, XXREAL_1: 3;

 then

 A26: (sX . a) = p by A6, FUNCT_1: 49;

 the carrier of ( I(01) | X) = X by PRE_TOPC: 8;

 then ( I(01) | X) = (( I[01] | F) | X9) by A10, A16, PRE_TOPC: 8, TSEP_1: 5;

 then

 A27: sX is continuous by A11, A14, Th41;



 A28: sX is one-to-one by A11, FUNCT_1: 52;



 then (sX " ) = (sX qua Function " ) by A24, TOPS_2:def 4

 .= ((s qua Function " ) | (s .: X)) by A11, RFUNCT_2: 17

 .= ((s " ) | ( [#] (( TOP-REAL n) | (A \ {q})))) by A25, A11, A22, TOPS_2:def 4

 .= ((s " ) | Ap) by PRE_TOPC:def 5;

 then (sX " ) is continuous by A12, A17, A18, Th41;

 then sX is being_homeomorphism by A23, A19, A27, A28, TOPS_2:def 5;

 hence thesis by A26;

 end;

 theorem :: BORSUK_4:51



 Th48: for n be Element of NAT , A,B be Subset of ( TOP-REAL n), p,q be Point of ( TOP-REAL n) st A is_an_arc_of (p,q) & B is_an_arc_of (q,p) & (A /\ B) = {p, q} & p <> q holds ( I(01) ,(( TOP-REAL n) | ((A \ {p}) \/ (B \ {p})))) are_homeomorphic

 proof

 reconsider a = 0 , b = (1 / 2), c = 1 as Point of I[01] by BORSUK_1: 43;

 let n be Element of NAT , A,B be Subset of ( TOP-REAL n), p,q be Point of ( TOP-REAL n);

 assume that

 A1: A is_an_arc_of (p,q) and

 A2: B is_an_arc_of (q,p) and

 A3: (A /\ B) = {p, q} and

 A4: p <> q;

 consider E2 be non empty Subset of I(01) , ty be Function of ( I(01) | E2), (( TOP-REAL n) | (B \ {p})) such that

 A5: E2 = [.b, c.[ and

 A6: ty is being_homeomorphism and

 A7: (ty . b) = q by A2, Th47;

 consider E1 be non empty Subset of I(01) , sx be Function of ( I(01) | E1), (( TOP-REAL n) | (A \ {p})) such that

 A8: E1 = ].a, b.] and

 A9: sx is being_homeomorphism and

 A10: (sx . b) = q by A1, Th46;

 set T1 = ( I(01) | E1), T2 = ( I(01) | E2), T = I(01) , S = (( TOP-REAL n) | ((A \ {p}) \/ (B \ {p}))), U1 = (( TOP-REAL n) | (A \ {p})), U2 = (( TOP-REAL n) | (B \ {p}));



 A11: (A \ {p}) is non empty by A1, Th3;

 then

 reconsider S as non empty SubSpace of ( TOP-REAL n);

 (B \ {p}) is non empty by A2, Th3, JORDAN5B: 14;

 then

 reconsider U1, U2 as non empty SubSpace of ( TOP-REAL n) by A11;



 A12: the carrier of S = ((A \ {p}) \/ (B \ {p})) by PRE_TOPC: 8;

 the carrier of U2 = (B \ {p}) by PRE_TOPC: 8;

 then

 A13: the carrier of U2 c= the carrier of S by A12, XBOOLE_1: 7;

 then

 reconsider ty9 = ty as Function of T2, S by FUNCT_2: 7;



 A14: U2 is SubSpace of S by A13, TSEP_1: 4;

 ty is continuous by A6, TOPS_2:def 5;

 then

 A15: ty9 is continuous by A14, PRE_TOPC: 26;

 reconsider F1 = ( [#] T1), F2 = ( [#] T2) as non empty Subset of T by PRE_TOPC:def 5;



 A16: F2 = [.(1 / 2), 1.[ by A5, PRE_TOPC:def 5;

 the carrier of U1 = (A \ {p}) by PRE_TOPC: 8;

 then

 A17: the carrier of U1 c= the carrier of S by A12, XBOOLE_1: 7;

 then

 reconsider sx9 = sx as Function of T1, S by FUNCT_2: 7;



 A18: U1 is SubSpace of S by A17, TSEP_1: 4;



 A19: ( rng ty) = ( [#] (( TOP-REAL n) | (B \ {p}))) by A6, TOPS_2:def 5;

 then

 A20: ( rng ty) = (B \ {p}) by PRE_TOPC:def 5;



 A21: ty is onto by A19, FUNCT_2:def 3;



 A22: ( rng sx) = ( [#] (( TOP-REAL n) | (A \ {p}))) by A9, TOPS_2:def 5;

 then

 A23: ( rng sx) = (A \ {p}) by PRE_TOPC:def 5;



 then

 A24: (( rng sx9) /\ ( rng ty9)) = (((A \ {p}) /\ B) \ {p}) by A20, XBOOLE_1: 49

 .= (((A /\ B) \ {p}) \ {p}) by XBOOLE_1: 49

 .= ((A /\ B) \ ( {p} \/ {p})) by XBOOLE_1: 41

 .= {(sx9 . b)} by A3, A4, A10, ZFMISC_1: 17;

 sx is continuous by A9, TOPS_2:def 5;

 then

 A25: sx9 is continuous by A18, PRE_TOPC: 26;



 A26: (1 / 2) in the carrier of I[01] by BORSUK_1: 43;

 then

 A27: F2 is closed by A16, Th45;



 A28: F1 = ]. 0 , (1 / 2).] by A8, PRE_TOPC:def 5;



 then

 A29: (( [#] T1) \/ ( [#] T2)) = ]. 0 , 1.[ by A16, XXREAL_1: 172

 .= ( [#] T) by Def1;



 A30: (( [#] T1) /\ ( [#] T2)) = {(1 / 2)} by A28, A16, XXREAL_1: 138;



 A31: for d be object st d in (( [#] T1) /\ ( [#] T2)) holds (sx . d) = (ty . d)

 proof

 let d be object;

 assume d in (( [#] T1) /\ ( [#] T2));

 then d = b by A30, TARSKI:def 1;

 hence thesis by A10, A7;

 end;

 F1 is closed by A26, A28, Th44;

 then

 consider F be Function of T, S such that

 A32: F = (sx9 +* ty) and

 A33: F is continuous by A25, A15, A27, A29, A31, JGRAPH_2: 1;



 A34: ( [#] U2) = (B \ {p}) by PRE_TOPC:def 5;

 then

 A35: ( [#] U2) c= ((A \ {p}) \/ (B \ {p})) by XBOOLE_1: 7;

 the carrier of T2 c= the carrier of T by BORSUK_1: 1;

 then

 reconsider g = (ty " ) as Function of U2, T by FUNCT_2: 7;

 the carrier of T1 c= the carrier of T by BORSUK_1: 1;

 then

 reconsider f = (sx " ) as Function of U1, T by FUNCT_2: 7;



 A36: ( dom ty9) = ( [#] T2) by FUNCT_2:def 1;



 A37: ( [#] U1) = (A \ {p}) by PRE_TOPC:def 5;

 then ( [#] U1) c= ((A \ {p}) \/ (B \ {p})) by XBOOLE_1: 7;

 then

 reconsider V1 = ( [#] U1), V2 = ( [#] U2) as Subset of S by A35, PRE_TOPC: 8;



 A38: ( dom F) = ( [#] I(01) ) by FUNCT_2:def 1;



 A39: V2 is closed

 proof

 reconsider B9 = B as Subset of ( TOP-REAL n);



 A40: B9 is closed by A2, COMPTS_1: 7, JORDAN5A: 1;



 A41: not p in {q} by A4, TARSKI:def 1;

 q in B by A2, TOPREAL1: 1;

 then

 A42: {q} c= B by ZFMISC_1: 31;



 A43: (B /\ (A \ {p})) = ((B /\ A) \ {p}) by XBOOLE_1: 49

 .= {q} by A3, A4, ZFMISC_1: 17;

 (B9 /\ ( [#] S)) = (B9 /\ ((A \ {p}) \/ (B \ {p}))) by PRE_TOPC:def 5

 .= ((B /\ (A \ {p})) \/ (B /\ (B \ {p}))) by XBOOLE_1: 23

 .= ((B /\ (A \ {p})) \/ (B \ {p})) by XBOOLE_1: 28, XBOOLE_1: 36

 .= (B \ {p}) by A41, A42, A43, XBOOLE_1: 12, ZFMISC_1: 34

 .= V2 by PRE_TOPC:def 5;

 hence thesis by A40, PRE_TOPC: 13;

 end;



 A44: V1 is closed

 proof

 reconsider A9 = A as Subset of ( TOP-REAL n);



 A45: A9 is closed by A1, COMPTS_1: 7, JORDAN5A: 1;



 A46: not p in {q} by A4, TARSKI:def 1;

 q in A by A1, TOPREAL1: 1;

 then

 A47: {q} c= A by ZFMISC_1: 31;



 A48: (A /\ (B \ {p})) = ((A /\ B) \ {p}) by XBOOLE_1: 49

 .= {q} by A3, A4, ZFMISC_1: 17;

 (A9 /\ ( [#] S)) = (A9 /\ ((A \ {p}) \/ (B \ {p}))) by PRE_TOPC:def 5

 .= ((A /\ (A \ {p})) \/ (A /\ (B \ {p}))) by XBOOLE_1: 23

 .= ((A \ {p}) \/ (A /\ (B \ {p}))) by XBOOLE_1: 28, XBOOLE_1: 36

 .= (A \ {p}) by A46, A47, A48, XBOOLE_1: 12, ZFMISC_1: 34

 .= V1 by PRE_TOPC:def 5;

 hence thesis by A45, PRE_TOPC: 13;

 end;

 (ty " ) is continuous by A6, TOPS_2:def 5;

 then

 A49: g is continuous by PRE_TOPC: 26;

 (sx " ) is continuous by A9, TOPS_2:def 5;

 then

 A50: f is continuous by PRE_TOPC: 26;



 A51: ty9 is one-to-one by A6, TOPS_2:def 5;

 then

 A52: (ty " ) = (ty qua Function " ) by A21, TOPS_2:def 4;



 A53: ( dom sx9) = ( [#] T1) by FUNCT_2:def 1;

 then

 A54: (( dom sx9) /\ ( dom ty9)) = {b} by A28, A16, A36, XXREAL_1: 138;

 sx9 tolerates ty9

 proof

 let t be object;

 assume t in (( dom sx9) /\ ( dom ty9));

 then t = b by A54, TARSKI:def 1;

 hence thesis by A10, A7;

 end;



 then

 A55: ( rng F) = (( rng sx9) \/ ( rng ty9)) by A32, FRECHET: 35

 .= ( [#] S) by A23, A20, PRE_TOPC:def 5;



 A56: sx is onto by A22, FUNCT_2:def 3;



 A57: sx9 is one-to-one by A9, TOPS_2:def 5;

 then

 A58: (sx " ) = (sx qua Function " ) by A56, TOPS_2:def 4;



 A59: for r be object st r in (( [#] U1) /\ ( [#] U2)) holds (f . r) = (g . r)

 proof

 let r be object;

 b in E2 by A5, XXREAL_1: 3;

 then

 A60: b in ( dom ty) by A36, PRE_TOPC:def 5;

 b in E1 by A8, XXREAL_1: 2;

 then b in ( dom sx) by A53, PRE_TOPC:def 5;

 then

 A61: (f . q) = b by A10, A57, A58, FUNCT_1: 34;

 assume r in (( [#] U1) /\ ( [#] U2));

 then r = q by A10, A22, A19, A24, TARSKI:def 1;

 hence thesis by A7, A51, A52, A60, A61, FUNCT_1: 34;

 end;

 (( [#] U1) \/ ( [#] U2)) = ( [#] S) by A37, A34, PRE_TOPC:def 5;

 then

 A62: ex h be Function of S, T st h = (f +* g) & h is continuous by A18, A14, A44, A39, A50, A49, A59, JGRAPH_2: 1;



 A63: F is onto by A55, FUNCT_2:def 3;



 A64: F is one-to-one by A32, A57, A51, A54, A24, Th1;

 then (F " ) = (F qua Function " ) by A63, TOPS_2:def 4;

 then (F " ) = ((sx " ) +* (ty " )) by A10, A7, A32, A57, A51, A54, A24, A58, A52, Th2;

 then F is being_homeomorphism by A33, A38, A64, A55, A62, TOPS_2:def 5;

 hence thesis by T_0TOPSP:def 1;

 end;

 theorem :: BORSUK_4:52



 Th49: for D be Simple_closed_curve, p be Point of ( TOP-REAL 2) st p in D holds ((( TOP-REAL 2) | (D \ {p})), I(01) ) are_homeomorphic

 proof

 let D be Simple_closed_curve, p be Point of ( TOP-REAL 2);

 consider q be Point of ( TOP-REAL 2) such that

 A1: q in D and

 A2: p <> q by SUBSET_1: 51;

 not q in {p} by A2, TARSKI:def 1;

 then

 reconsider R2p = (D \ {p}) as non empty Subset of ( TOP-REAL 2) by A1, XBOOLE_0:def 5;

 assume p in D;

 then

 consider P1,P2 be non empty Subset of ( TOP-REAL 2) such that

 A3: P1 is_an_arc_of (p,q) and

 A4: P2 is_an_arc_of (p,q) and

 A5: D = (P1 \/ P2) and

 A6: (P1 /\ P2) = {p, q} by A1, A2, TOPREAL2: 5;



 A7: P2 is_an_arc_of (q,p) by A4, JORDAN5B: 14;

 (D \ {p}) = ((P1 \ {p}) \/ (P2 \ {p})) by A5, XBOOLE_1: 42;

 then ((( TOP-REAL 2) | R2p), I(01) ) are_homeomorphic by A2, A3, A6, A7, Th48;

 hence thesis;

 end;

 theorem :: BORSUK_4:53

 for D be Simple_closed_curve, p,q be Point of ( TOP-REAL 2) st p in D & q in D holds ((( TOP-REAL 2) | (D \ {p})),(( TOP-REAL 2) | (D \ {q}))) are_homeomorphic

 proof

 let D be Simple_closed_curve, p,q be Point of ( TOP-REAL 2);

 assume that

 A1: p in D and

 A2: q in D;

 per cases ;

 suppose p = q;

 hence thesis;

 end;

 suppose p <> q;

 then

 reconsider Dp = (D \ {p}), Dq = (D \ {q}) as non empty Subset of ( TOP-REAL 2) by A1, A2, ZFMISC_1: 56;



 A3: ((( TOP-REAL 2) | Dq), I(01) ) are_homeomorphic by A2, Th49;

 ((( TOP-REAL 2) | Dp), I(01) ) are_homeomorphic by A1, Th49;

 hence thesis by A3, BORSUK_3: 3;

 end;

 end;

 theorem :: BORSUK_4:54



 Th51: for n be Element of NAT , C be non empty Subset of ( TOP-REAL n), E be Subset of I(01) st (ex p1,p2 be Point of I[01] st p1 < p2 & E = [.p1, p2.]) & (( I(01) | E),(( TOP-REAL n) | C)) are_homeomorphic holds ex s1,s2 be Point of ( TOP-REAL n) st C is_an_arc_of (s1,s2)

 proof

 let n be Element of NAT , C be non empty Subset of ( TOP-REAL n), E be Subset of I(01) ;

 given p1,p2 be Point of I[01] such that

 A1: p1 < p2 and

 A2: E = [.p1, p2.];



 A3: ( I[01] ,( I(01) | E)) are_homeomorphic by A1, A2, Th39;

 assume

 A4: (( I(01) | E),(( TOP-REAL n) | C)) are_homeomorphic ;

 E is non empty by A1, A2, Th21;

 then ( I[01] ,(( TOP-REAL n) | C)) are_homeomorphic by A4, A3, BORSUK_3: 3;

 then

 consider g be Function of I[01] , (( TOP-REAL n) | C) such that

 A5: g is being_homeomorphism by T_0TOPSP:def 1;

 set s1 = (g . 0 ), s2 = (g . 1);

 0 in the carrier of I[01] by BORSUK_1: 43;

 then

 A6: (g . 0 ) in the carrier of (( TOP-REAL n) | C) by FUNCT_2: 5;

 1 in the carrier of I[01] by BORSUK_1: 43;

 then

 A7: (g . 1) in the carrier of (( TOP-REAL n) | C) by FUNCT_2: 5;

 the carrier of (( TOP-REAL n) | C) c= the carrier of ( TOP-REAL n) by BORSUK_1: 1;

 then

 reconsider s1, s2 as Point of ( TOP-REAL n) by A6, A7;

 C is_an_arc_of (s1,s2) by A5, TOPREAL1:def 1;

 hence thesis;

 end;

 theorem :: BORSUK_4:55



 Th52: for Dp be non empty Subset of ( TOP-REAL 2), f be Function of (( TOP-REAL 2) | Dp), I(01) , C be non empty Subset of ( TOP-REAL 2) st f is being_homeomorphism & C c= Dp & (ex p1,p2 be Point of I[01] st p1 < p2 & (f .: C) = [.p1, p2.]) holds ex s1,s2 be Point of ( TOP-REAL 2) st C is_an_arc_of (s1,s2)

 proof

 let Dp be non empty Subset of ( TOP-REAL 2), f be Function of (( TOP-REAL 2) | Dp), I(01) , C be non empty Subset of ( TOP-REAL 2);

 assume that

 A1: f is being_homeomorphism and

 A2: C c= Dp;

 reconsider C9 = C as Subset of (( TOP-REAL 2) | Dp) by A2, PRE_TOPC: 8;



 A3: the carrier of (( TOP-REAL 2) | Dp) = Dp by PRE_TOPC: 8;

 ( dom f) = the carrier of (( TOP-REAL 2) | Dp) by FUNCT_2:def 1;

 then C c= ( dom f) by A2, PRE_TOPC: 8;

 then

 A4: C c= (f " (f .: C)) by FUNCT_1: 76;

 given p1,p2 be Point of I[01] such that

 A5: p1 < p2 and

 A6: (f .: C) = [.p1, p2.];

 reconsider E = [.p1, p2.] as Subset of I(01) by A6;



 A7: ( rng f) = ( [#] I(01) ) by A1, TOPS_2:def 5;



 A8: f is continuous one-to-one by A1, TOPS_2:def 5;

 then (f " (f .: C)) c= C by FUNCT_1: 82;

 then (f " (f .: C)) = C by A4, XBOOLE_0:def 10;

 then

 A9: ((f " ) .: E) = C by A6, A8, A7, TOPS_2: 55;

 the carrier of (( TOP-REAL 2) | C) = C by PRE_TOPC: 8;

 then

 A10: (( TOP-REAL 2) | C) is SubSpace of (( TOP-REAL 2) | Dp) by A2, A3, TOPMETR: 3;

 set g = ((f " ) | E);

 the carrier of ( I(01) | E) = E by PRE_TOPC: 8;

 then

 A11: g is Function of the carrier of ( I(01) | E), the carrier of (( TOP-REAL 2) | Dp) by FUNCT_2: 32;



 A12: ( rng g) = ((f " ) .: E) by RELAT_1: 115

 .= ( [#] (( TOP-REAL 2) | C)) by A9, PRE_TOPC: 8;

 then

 reconsider g as Function of ( I(01) | E), (( TOP-REAL 2) | C) by A11, FUNCT_2: 6;

 (f " ) is being_homeomorphism by A1, TOPS_2: 56;

 then

 A13: (f " ) is one-to-one by TOPS_2:def 5;

 then

 A14: g is one-to-one by FUNCT_1: 52;



 A15: f is onto by A7, FUNCT_2:def 3;

 g is onto by A12, FUNCT_2:def 3;



 then

 A16: (g " ) = (g qua Function " ) by A14, TOPS_2:def 4

 .= (((f " ) qua Function " ) | ((f " ) .: E)) by A13, RFUNCT_2: 17

 .= (((f qua Function " ) " ) | ((f " ) .: E)) by A8, A15, TOPS_2:def 4

 .= (f | C) by A8, A9, FUNCT_1: 43;

 then

 reconsider t = (f | C) as Function of (( TOP-REAL 2) | C), ( I(01) | E);

 ( dom (f " )) = the carrier of I(01) by FUNCT_2:def 1;



 then ( dom g) = E by RELAT_1: 62

 .= the carrier of ( I(01) | E) by PRE_TOPC: 8;

 then

 A17: ( dom g) = ( [#] ( I(01) | E));

 (f " ) is continuous by A1, TOPS_2:def 5;

 then

 A18: g is continuous by A10, Th41;

 ((( TOP-REAL 2) | Dp) | C9) = (( TOP-REAL 2) | C) by A2, PRE_TOPC: 7;

 then t is continuous by A8, Th41;

 then g is being_homeomorphism by A12, A17, A14, A18, A16, TOPS_2:def 5;

 then (( I(01) | E),(( TOP-REAL 2) | C)) are_homeomorphic by T_0TOPSP:def 1;

 hence thesis by A5, Th51;

 end;

 theorem :: BORSUK_4:56

 for D be Simple_closed_curve, C be non empty compact connected Subset of ( TOP-REAL 2) st C c= D holds C = D or (ex p1,p2 be Point of ( TOP-REAL 2) st C is_an_arc_of (p1,p2)) or ex p be Point of ( TOP-REAL 2) st C = {p}

 proof

 let D be Simple_closed_curve, C be non empty compact connected Subset of ( TOP-REAL 2);

 assume

 A1: C c= D;

 assume

 A2: C <> D;

 per cases ;

 suppose C is trivial;

 hence thesis by SUBSET_1: 47;

 end;

 suppose

 A3: C is non trivial;

 C c< D by A1, A2, XBOOLE_0:def 8;

 then

 consider p be Point of ( TOP-REAL 2) such that

 A4: p in D and

 A5: C c= (D \ {p}) by SUBSET_1: 44;

 consider d1,d2 be Point of ( TOP-REAL 2) such that

 A6: d1 in C and

 A7: d2 in C and

 A8: d1 <> d2 by A3, SUBSET_1: 45;

 reconsider Dp = (D \ {p}) as non empty Subset of ( TOP-REAL 2) by A5;

 ((( TOP-REAL 2) | Dp), I(01) ) are_homeomorphic by A4, Th49;

 then

 consider f be Function of (( TOP-REAL 2) | Dp), I(01) such that

 A9: f is being_homeomorphism by T_0TOPSP:def 1;

 reconsider C9 = C as Subset of (( TOP-REAL 2) | Dp) by A5, PRE_TOPC: 8;

 C c= ( [#] (( TOP-REAL 2) | Dp)) by A5, PRE_TOPC: 8;

 then

 A10: C9 is compact by COMPTS_1: 2;

 set fC = (f .: C9);



 A11: C9 is connected by CONNSP_1: 23;



 A12: ( rng f) = ( [#] I(01) ) by A9, TOPS_2:def 5;

 f is continuous by A9, TOPS_2:def 5;

 then

 reconsider fC as compact connected Subset of I(01) by A10, A11, A12, COMPTS_1: 15, TOPS_2: 61;

 reconsider fC9 = fC as Subset of I[01] by PRE_TOPC: 11;



 A13: fC9 c= ( [#] I(01) );



 A14: for P be Subset of I(01) st P = fC9 holds P is compact;

 d1 in (D \ {p}) by A6, A5;

 then d1 in the carrier of (( TOP-REAL 2) | Dp) by PRE_TOPC: 8;

 then

 A15: d1 in ( dom f) by FUNCT_2:def 1;



 A16: f is one-to-one by A9, TOPS_2:def 5;

 d2 in (D \ {p}) by A7, A5;

 then d2 in the carrier of (( TOP-REAL 2) | Dp) by PRE_TOPC: 8;

 then

 A17: d2 in ( dom f) by FUNCT_2:def 1;



 A18: (f . d2) in (f .: C9) by A7, FUNCT_2: 35;

 then

 reconsider fC9 as non empty compact connected Subset of I[01] by A13, A14, COMPTS_1: 2, CONNSP_1: 23;

 consider p1,p2 be Point of I[01] such that

 A19: p1 <= p2 and

 A20: fC9 = [.p1, p2.] by Th28;



 A21: (f . d1) in (f .: C9) by A6, FUNCT_2: 35;

 p1 <> p2

 proof

 assume p1 = p2;

 then

 A22: fC9 = {p1} by A20, XXREAL_1: 17;

 then

 A23: (f . d2) = p1 by A18, TARSKI:def 1;

 (f . d1) = p1 by A21, A22, TARSKI:def 1;

 hence thesis by A8, A15, A17, A16, A23, FUNCT_1:def 4;

 end;

 then p1 < p2 by A19, XXREAL_0: 1;

 hence thesis by A5, A9, A20, Th52;

 end;

 end;

 begin

 theorem :: BORSUK_4:57



 Th54: for C be non empty compact Subset of I[01] st C c= ]. 0 , 1.[ holds ex D be non empty closed_interval Subset of REAL st C c= D & D c= ]. 0 , 1.[ & ( lower_bound C) = ( lower_bound D) & ( upper_bound C) = ( upper_bound D)

 proof

 let C be non empty compact Subset of I[01] ;

 assume

 A1: C c= ]. 0 , 1.[;

 reconsider C9 = C as Subset of REAL by BORSUK_1: 40, XBOOLE_1: 1;

 reconsider D = [.( lower_bound C9), ( upper_bound C9).] as Subset of REAL ;



 A2: C9 is bounded_below bounded_above by Th22;

 then

 A3: ( lower_bound C9) <= ( upper_bound C9) by SEQ_4: 11;



 A4: C c= D

 proof

 let x be object;

 assume

 A5: x in C;

 then x in the carrier of I[01] ;

 then

 reconsider x9 = x as Real;



 A6: x9 <= ( upper_bound C9) by A5, Th23;

 ( lower_bound C9) <= x9 by A5, Th23;

 hence thesis by A6, XXREAL_1: 1;

 end;



 A7: C9 is closed by Th24;

 then

 A8: ( lower_bound C9) in C9 by Th22, RCOMP_1: 13;



 A9: ( upper_bound C9) in C9 by A7, Th22, RCOMP_1: 12;

 then

 A10: D is non empty compact connected Subset of I[01] by A2, A8, Th21, SEQ_4: 11;

 then

 A11: D is non empty closed_interval Subset of REAL by Th27;

 then

 A12: D = [.( lower_bound D), ( upper_bound D).] by INTEGRA1: 4;

 then

 A13: ( upper_bound C9) = ( upper_bound D) by A3, XXREAL_1: 66;



 A14: not 1 in D

 proof

 assume 1 in D;

 then ( upper_bound D) >= 1 by A11, INTEGRA2: 1;

 hence thesis by A1, A9, A13, XXREAL_1: 4;

 end;



 A15: ( lower_bound C9) = ( lower_bound D) by A3, A12, XXREAL_1: 66;



 A16: not 0 in D

 proof

 assume 0 in D;

 then ( lower_bound D) <= 0 by A11, INTEGRA2: 1;

 hence thesis by A1, A8, A15, XXREAL_1: 4;

 end;



 A17: D c= ]. 0 , 1.[ by A10, A16, A14, BORSUK_1: 40, XXREAL_1: 5;

 reconsider D as non empty closed_interval Subset of REAL by A3, MEASURE5: 14;

 take D;

 thus thesis by A4, A3, A12, A17, XXREAL_1: 66;

 end;

 theorem :: BORSUK_4:58



 Th55: for C be non empty compact Subset of I[01] st C c= ]. 0 , 1.[ holds ex p1,p2 be Point of I[01] st p1 <= p2 & C c= [.p1, p2.] & [.p1, p2.] c= ]. 0 , 1.[

 proof

 let C be non empty compact Subset of I[01] ;

 assume C c= ]. 0 , 1.[;

 then

 consider D be non empty closed_interval Subset of REAL such that

 A1: C c= D and

 A2: D c= ]. 0 , 1.[ and ( lower_bound C) = ( lower_bound D) and ( upper_bound C) = ( upper_bound D) by Th54;

 consider p1,p2 be Real such that

 A3: p1 <= p2 and

 A4: D = [.p1, p2.] by MEASURE5: 14;

 p1 in D by A3, A4, XXREAL_1: 1;

 then

 A5: p1 in ]. 0 , 1.[ by A2;

 p2 in D by A3, A4, XXREAL_1: 1;

 then

 A6: p2 in ]. 0 , 1.[ by A2;

 ]. 0 , 1.[ c= [. 0 , 1.] by XXREAL_1: 25;

 then

 reconsider p1, p2 as Point of I[01] by A5, A6, BORSUK_1: 40;

 take p1, p2;

 thus p1 <= p2 by A3;

 thus thesis by A1, A2, A4;

 end;

 theorem :: BORSUK_4:59

 for D be Simple_closed_curve, C be closed Subset of ( TOP-REAL 2) st C c< D holds ex p1,p2 be Point of ( TOP-REAL 2), B be Subset of ( TOP-REAL 2) st B is_an_arc_of (p1,p2) & C c= B & B c= D

 proof

 let D be Simple_closed_curve, C be closed Subset of ( TOP-REAL 2);

 assume

 A1: C c< D;

 then

 A2: C c= D by XBOOLE_0:def 8;



 A3: for C be compact Subset of ( TOP-REAL 2) st C is non trivial & C c< D holds ex p1,p2 be Point of ( TOP-REAL 2), B be Subset of ( TOP-REAL 2) st B is_an_arc_of (p1,p2) & C c= B & B c= D

 proof

 let C be compact Subset of ( TOP-REAL 2);

 assume C is non trivial;

 then

 consider d1,d2 be Point of ( TOP-REAL 2) such that

 A4: d1 in C and

 A5: d2 in C and

 A6: d1 <> d2 by SUBSET_1: 45;

 assume C c< D;

 then

 consider p be Point of ( TOP-REAL 2) such that

 A7: p in D and

 A8: C c= (D \ {p}) by A4, SUBSET_1: 44;

 reconsider Dp = (D \ {p}) as non empty Subset of ( TOP-REAL 2) by A4, A8;

 ((( TOP-REAL 2) | Dp), I(01) ) are_homeomorphic by A7, Th49;

 then

 consider f be Function of (( TOP-REAL 2) | Dp), I(01) such that

 A9: f is being_homeomorphism by T_0TOPSP:def 1;

 d2 in (D \ {p}) by A5, A8;

 then d2 in the carrier of (( TOP-REAL 2) | Dp) by PRE_TOPC: 8;

 then

 A10: d2 in ( dom f) by FUNCT_2:def 1;

 d1 in (D \ {p}) by A4, A8;

 then d1 in the carrier of (( TOP-REAL 2) | Dp) by PRE_TOPC: 8;

 then

 A11: d1 in ( dom f) by FUNCT_2:def 1;



 A12: f is one-to-one by A9, TOPS_2:def 5;

 C c= the carrier of (( TOP-REAL 2) | Dp) by A8, PRE_TOPC: 8;

 then

 A13: C c= ( dom f) by FUNCT_2:def 1;

 ( dom f) = the carrier of (( TOP-REAL 2) | Dp) by FUNCT_2:def 1;

 then

 A14: ( dom f) c= the carrier of ( TOP-REAL 2) by BORSUK_1: 1;

 ( dom f) = the carrier of (( TOP-REAL 2) | Dp) by FUNCT_2:def 1;

 then

 A15: ( dom f) = Dp by PRE_TOPC: 8;

 reconsider C9 = C as Subset of (( TOP-REAL 2) | Dp) by A8, PRE_TOPC: 8;

 C c= ( [#] (( TOP-REAL 2) | Dp)) by A8, PRE_TOPC: 8;

 then

 A16: C9 is compact by COMPTS_1: 2;

 set fC = (f .: C9);



 A17: ( rng f) = ( [#] I(01) ) by A9, TOPS_2:def 5;

 f is continuous by A9, TOPS_2:def 5;

 then

 reconsider fC as compact Subset of I(01) by A16, A17, COMPTS_1: 15;

 reconsider fC9 = fC as Subset of I[01] by PRE_TOPC: 11;



 A18: fC9 c= ( [#] I(01) );



 A19: for P be Subset of I(01) st P = fC9 holds P is compact;

 fC9 c= the carrier of I(01) ;

 then

 A20: fC9 c= ]. 0 , 1.[ by Def1;



 A21: (f . d2) in (f .: C9) by A5, FUNCT_2: 35;

 then

 reconsider fC9 as non empty compact Subset of I[01] by A18, A19, COMPTS_1: 2;

 consider p1,p2 be Point of I[01] such that

 A22: p1 <= p2 and

 A23: fC9 c= [.p1, p2.] and

 A24: [.p1, p2.] c= ]. 0 , 1.[ by A20, Th55;

 reconsider E = [.p1, p2.] as non empty compact connected Subset of I[01] by A22, Th21;



 A25: (f " E) c= ( dom f) by RELAT_1: 132;



 A26: (f . d1) in (f .: C9) by A4, FUNCT_2: 35;

 p1 <> p2

 proof

 assume p1 = p2;

 then

 A27: fC9 c= {p1} by A23, XXREAL_1: 17;

 then

 A28: (f . d2) = p1 by A21, TARSKI:def 1;

 (f . d1) = p1 by A26, A27, TARSKI:def 1;

 hence thesis by A6, A11, A10, A12, A28, FUNCT_1:def 4;

 end;

 then

 A29: p1 < p2 by A22, XXREAL_0: 1;

 E c= ( rng f) by A17, A24, Def1;

 then

 reconsider B = (f " E) as non empty Subset of ( TOP-REAL 2) by A25, A14, RELAT_1: 139, XBOOLE_1: 1;

 ( rng f) = ]. 0 , 1.[ by A17, Def1;

 then (f .: (f " E)) = E by A24, FUNCT_1: 77;

 then

 consider s1,s2 be Point of ( TOP-REAL 2) such that

 A30: B is_an_arc_of (s1,s2) by A9, A29, A15, Th52, RELAT_1: 132;

 take s1, s2, B;

 thus B is_an_arc_of (s1,s2) by A30;

 Dp c= D by XBOOLE_1: 36;

 hence thesis by A23, A25, A15, A13, FUNCT_1: 93;

 end;



 A31: C is compact by A2, RLTOPSP1: 42, TOPREAL6: 79;

 per cases ;

 suppose

 A32: C is trivial;

 per cases ;

 suppose

 A33: C = {} ;

 consider p,q be Point of ( TOP-REAL 2) such that

 A34: p <> q and

 A35: p in D and

 A36: q in D by TOPREAL2: 4;

 reconsider CC = {p, q} as Subset of ( TOP-REAL 2);



 A37: q in CC by TARSKI:def 2;

 p in CC by TARSKI:def 2;

 then

 A38: CC is non trivial by A34, A37;

 reconsider pp = {p}, qq = {q} as Subset of ( TOP-REAL 2);

 CC = (pp \/ qq) by ENUMSET1: 1;

 then

 A39: CC is compact by COMPTS_1: 10;



 A40: CC <> D

 proof

 assume CC = D;

 then (D \ CC) = {} by XBOOLE_1: 37;

 then not ( {} (( TOP-REAL 2) | D)) is connected by A34, A35, A36, JORDAN6: 47;

 hence thesis;

 end;

 CC c= D by A35, A36, ZFMISC_1: 32;

 then CC c< D by A40, XBOOLE_0:def 8;

 then

 consider p1,p2 be Point of ( TOP-REAL 2), B be Subset of ( TOP-REAL 2) such that

 A41: B is_an_arc_of (p1,p2) and CC c= B and

 A42: B c= D by A3, A38, A39;

 take p1, p2, B;

 thus B is_an_arc_of (p1,p2) by A41;

 thus C c= B by A33;

 thus thesis by A42;

 end;

 suppose C <> {} ;

 then

 consider x be Element of ( TOP-REAL 2) such that

 A43: C = {x} by A32, SUBSET_1: 47;

 consider y be Element of D such that

 A44: x <> y by SUBSET_1: 50;

 reconsider y9 = y as Element of ( TOP-REAL 2);

 reconsider Y = {y9} as compact non empty Subset of ( TOP-REAL 2);

 reconsider Cy = (C \/ Y) as non empty compact Subset of ( TOP-REAL 2) by A31, COMPTS_1: 10;



 A45: x in C by A43, TARSKI:def 1;



 A46: Cy <> D

 proof

 assume Cy = D;

 then

 A47: (D \ Cy) = {} by XBOOLE_1: 37;

 Cy = {x, y} by A43, ENUMSET1: 1;

 then not ( {} (( TOP-REAL 2) | D)) is connected by A2, A45, A44, A47, JORDAN6: 47;

 hence thesis;

 end;

 {y} c= D;

 then Cy c= D by A2, XBOOLE_1: 8;

 then

 A48: Cy c< D by A46, XBOOLE_0:def 8;



 A49: C c= Cy by XBOOLE_1: 7;

 y in Y by TARSKI:def 1;

 then y in Cy by XBOOLE_0:def 3;

 then Cy is non trivial by A45, A44, A49;

 then

 consider p1,p2 be Point of ( TOP-REAL 2), B be Subset of ( TOP-REAL 2) such that

 A50: B is_an_arc_of (p1,p2) and

 A51: Cy c= B and

 A52: B c= D by A3, A48;

 take p1, p2, B;

 thus B is_an_arc_of (p1,p2) by A50;

 thus C c= B by A49, A51;

 thus thesis by A52;

 end;

 end;

 suppose C is non trivial;

 hence thesis by A1, A31, A3;

 end;

 end;