:: BORSUK_4 semantic presentation

begin

registration
cluster being_simple_closed_curve  ->  non trivial for Element of bool the carrier of (TOP-REAL 2);
coherence
 for b1 being Simple_closed_curve holds not b1 is trivial
proof
let D be Simple_closed_curve; ::_thesis: not D is trivial
 ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in D & p2 in D ) by TOPREAL2:5;
hence  not D is trivial by ZFMISC_1:def_10; ::_thesis: verum
end;
end;

theorem Th1: :: BORSUK_4:1
for X being non empty set
for A being non empty Subset of X st A is trivial holds
ex x being Element of X st A = {x} by SUBSET_1:47;

theorem Th2: :: BORSUK_4:2
for X being non trivial set
for p being set ex q being Element of X st q <> p
proof
let X be non trivial set ; ::_thesis: for p being set ex q being Element of X st q <> p
let p be set ; ::_thesis: ex q being Element of X st q <> p
 not X \ {p} is empty by REALSET1:3;
then consider q being set  such that
A1: q in X \ {p} by XBOOLE_0:def_1;
reconsider q = q as Element of X by A1;
take  q ; ::_thesis: q <> p
thus  q <> p by A1, ZFMISC_1:56; ::_thesis: verum
end;

theorem Th3: :: BORSUK_4:3
for T being non trivial set
for X being non trivial Subset of T
for p being set ex q being Element of T st
( q in X & q <> p )
proof
let T be non trivial set ; ::_thesis: for X being non trivial Subset of T
for p being set ex q being Element of T st
( q in X & q <> p )
let X be non trivial Subset of T; ::_thesis: for p being set ex q being Element of T st
( q in X & q <> p )
let p be set ; ::_thesis: ex q being Element of T st
( q in X & q <> p )
set p9 = p;
 not X \ {p} is empty by REALSET1:3;
then consider q being set  such that
A1: q in X \ {p} by XBOOLE_0:def_1;
reconsider q = q as Element of T by A1;
take  q ; ::_thesis: ( q in X & q <> p )
thus  ( q in X & q <> p ) by A1, ZFMISC_1:56; ::_thesis: verum
end;

theorem Th4: :: BORSUK_4:4
for f, g being Function
for a being 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; ::_thesis: for a being 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
let a be set ; ::_thesis: ( f is one-to-one & g is one-to-one & (dom f) /\ (dom g) = {a} & (rng f) /\ (rng g) = {(f . a)} implies f +* g is one-to-one )
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)} ; ::_thesis: f +* g is one-to-one
 for x1, x2 being 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 ; ::_thesis: ( x1 in dom g & x2 in (dom f) \ (dom g) implies g . x1 <> f . x2 )
assume that
A7: x1 in dom g and
A8: x2 in (dom f) \ (dom g) ; ::_thesis: g . x1 <> f . x2
A9: f . x2 in rng f by A8, FUNCT_1:3;
assume A10: g . x1 = f . x2 ; ::_thesis: contradiction
 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  contradiction by XBOOLE_1:79; ::_thesis: verum
end;
hence  f +* g is one-to-one by A1, A2, TOPMETR2:1; ::_thesis: verum
end;

theorem Th5: :: BORSUK_4:5
for f, g being Function
for a being 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; ::_thesis: for a being 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 ")
let a be set ; ::_thesis: ( 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 implies (f +* g) " = (f ") +* (g ") )
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 ; ::_thesis: (f +* g) " = (f ") +* (g ")
A6: dom (g ") = rng g by A2, FUNCT_1:33;
A7: dom (f ") = rng f by A1, FUNCT_1:33;
 for x being set st x in (dom (f ")) /\ (dom (g ")) holds
(f ") . x = (g ") . x
proof
let x be set ; ::_thesis: ( x in (dom (f ")) /\ (dom (g ")) implies (f ") . x = (g ") . x )
 {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 ")) ; ::_thesis: (f ") . x = (g ") . x
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  (f ") . x = (g ") . x by A2, A11, A10, FUNCT_1:32; ::_thesis: verum
end;
then A12: f " tolerates g " by PARTFUN1:def_4;
set gf = (f ") +* (g ");
set F = f +* g;
 for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x )
assume  x in (dom f) /\ (dom g) ; ::_thesis: f . x = g . x
then  x = a by A3, TARSKI:def_1;
hence  f . x = g . x by A5; ::_thesis: verum
end;
then A13: f tolerates g by PARTFUN1:def_4;
dom ((f ") +* (g ")) = (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 ((f ") +* (g ")) = rng (f +* g) by A13, FRECHET:35;
A15: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def_1;
then A16: dom f c= dom (f +* g) by XBOOLE_1:7;
A17: dom g c= dom (f +* g) by A15, XBOOLE_1:7;
A18: rng (f +* g) = (rng f) \/ (rng g) by A13, FRECHET:35;
A19: for y, x being set holds
( y in rng (f +* g) & x = ((f ") +* (g ")) . y iff ( x in dom (f +* g) & y = (f +* g) . x ) )
proof
let y, x be set ; ::_thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y iff ( x in dom (f +* g) & y = (f +* g) . x ) )
hereby  ::_thesis: ( x in dom (f +* g) & y = (f +* g) . x implies ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) )
assume that
A20: y in rng (f +* g) and
A21: x = ((f ") +* (g ")) . y ; ::_thesis: ( x in dom (f +* g) & y = (f +* g) . x )
percases ( y in dom (f ") or y in dom (g ") ) by A14, A20, FUNCT_4:12;
supposeA22: y in dom (f ") ; ::_thesis: ( x in dom (f +* g) & y = (f +* g) . x )
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 +* g) & y = (f +* g) . x ) by A13, A16, A25, FUNCT_4:15; ::_thesis: verum
end;
supposeA26: y in dom (g ") ; ::_thesis: ( x in dom (f +* g) & y = (f +* g) . x )
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 +* g) & y = (f +* g) . x ) by A17, A29, FUNCT_4:13; ::_thesis: verum
end;
end;
end;
assume that
A30: x in dom (f +* g) and
A31: y = (f +* g) . x ; ::_thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y )
percases ( x in dom f or x in dom g ) by A30, FUNCT_4:12;
supposeA32: x in dom f ; ::_thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y )
then A33: y = f . x by A13, A31, FUNCT_4:15;
then A34: x = (f ") . y by A1, A32, FUNCT_1:32;
 rng (f +* g) = (rng f) \/ (rng g) by A13, FRECHET:35;
then A35: rng f c= rng (f +* g) 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  ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) by A12, A34, A36, A35, FUNCT_4:15; ::_thesis: verum
end;
supposeA37: x in dom g ; ::_thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y )
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 +* g) 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  ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) by A39, A41, A40, FUNCT_4:13; ::_thesis: verum
end;
end;
end;
 f +* g is one-to-one by A1, A2, A3, A4, Th4;
hence  (f +* g) " = (f ") +* (g ") by A14, A19, FUNCT_1:32; ::_thesis: verum
end;

theorem Th6: :: BORSUK_4:6
for n being Element of NAT
for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st A is_an_arc_of p,q holds
not A \ {p} is empty
proof
let n be Element of NAT ; ::_thesis: for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st A is_an_arc_of p,q holds
not A \ {p} is empty
let A be Subset of (TOP-REAL n); ::_thesis: for p, q being Point of (TOP-REAL n) st A is_an_arc_of p,q holds
not A \ {p} is empty
let p, q be Point of (TOP-REAL n); ::_thesis: ( A is_an_arc_of p,q implies not A \ {p} is empty )
assume  A is_an_arc_of p,q ; ::_thesis: not A \ {p} is empty
then A1: A \ {p,q} <> {} by JORDAN6:43;
 {p} c= {p,q} by ZFMISC_1:7;
hence  not A \ {p} is empty by A1, XBOOLE_1:3, XBOOLE_1:34; ::_thesis: verum
end;

theorem :: BORSUK_4:7
for s1, s3, s4, l being real number st s1 <= s3 & s1 < s4 & 0 <= l & l <= 1 holds
s1 <= ((1 - l) * s3) + (l * s4)
proof
let s1, s3, s4, l be real number ; ::_thesis: ( s1 <= s3 & s1 < s4 & 0 <= l & l <= 1 implies s1 <= ((1 - l) * s3) + (l * s4) )
assume that
A1: s1 <= s3 and
A2: s1 < s4 and
A3: 0 <= l and
A4: l <= 1 ; ::_thesis: s1 <= ((1 - l) * s3) + (l * s4)
now__::_thesis:_s1_<=_((1_-_l)_*_s3)_+_(l_*_s4)
percases ( l = 0 or l = 1 or ( not l = 0 & not l = 1 ) ) ;
suppose l = 0 ; ::_thesis: s1 <= ((1 - l) * s3) + (l * s4)
hence  s1 <= ((1 - l) * s3) + (l * s4) by A1; ::_thesis: verum
end;
suppose l = 1 ; ::_thesis: s1 <= ((1 - l) * s3) + (l * s4)
hence  s1 <= ((1 - l) * s3) + (l * s4) by A2; ::_thesis: verum
end;
supposeA5: ( not l = 0 & not l = 1 ) ; ::_thesis: s1 <= ((1 - l) * s3) + (l * s4)
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  s1 <= ((1 - l) * s3) + (l * s4) by A6, A7, XREAL_1:8; ::_thesis: verum
end;
end;
end;
hence  s1 <= ((1 - l) * s3) + (l * s4) ; ::_thesis: verum
end;

theorem Th8: :: BORSUK_4:8
for A being Subset of I[01]
for a, b being real number st a < b & A = ].a,b.[ holds
[.a,b.] c= the carrier of I[01]
proof
let A be Subset of I[01]; ::_thesis: for a, b being real number st a < b & A = ].a,b.[ holds
[.a,b.] c= the carrier of I[01]
let a, b be real number ; ::_thesis: ( a < b & A = ].a,b.[ implies [.a,b.] c= the carrier of I[01] )
assume A1: a < b ; ::_thesis: ( not A = ].a,b.[ or [.a,b.] c= the carrier of I[01] )
assume A2: A = ].a,b.[ ; ::_thesis: [.a,b.] c= the carrier of I[01]
then A3: b <= 1 by A1, BORSUK_1:40, XXREAL_1:51;
 0 <= a by A1, A2, BORSUK_1:40, XXREAL_1:51;
hence  [.a,b.] c= the carrier of I[01] by A3, BORSUK_1:40, XXREAL_1:34; ::_thesis: verum
end;

theorem Th9: :: BORSUK_4:9
for A being Subset of I[01]
for a, b being real number st a < b & A = ].a,b.] holds
[.a,b.] c= the carrier of I[01]
proof
let A be Subset of I[01]; ::_thesis: for a, b being real number st a < b & A = ].a,b.] holds
[.a,b.] c= the carrier of I[01]
let a, b be real number ; ::_thesis: ( a < b & A = ].a,b.] implies [.a,b.] c= the carrier of I[01] )
assume A1: a < b ; ::_thesis: ( not A = ].a,b.] or [.a,b.] c= the carrier of I[01] )
A2: ].a,b.[ c= ].a,b.] by XXREAL_1:21;
assume  A = ].a,b.] ; ::_thesis: [.a,b.] c= the carrier of I[01]
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  [.a,b.] c= the carrier of I[01] by A4, BORSUK_1:40, XXREAL_1:34; ::_thesis: verum
end;

theorem Th10: :: BORSUK_4:10
for A being Subset of I[01]
for a, b being real number st a < b & A = [.a,b.[ holds
[.a,b.] c= the carrier of I[01]
proof
let A be Subset of I[01]; ::_thesis: for a, b being real number st a < b & A = [.a,b.[ holds
[.a,b.] c= the carrier of I[01]
let a, b be real number ; ::_thesis: ( a < b & A = [.a,b.[ implies [.a,b.] c= the carrier of I[01] )
assume A1: a < b ; ::_thesis: ( not A = [.a,b.[ or [.a,b.] c= the carrier of I[01] )
A2: ].a,b.[ c= [.a,b.[ by XXREAL_1:22;
assume  A = [.a,b.[ ; ::_thesis: [.a,b.] c= the carrier of I[01]
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  [.a,b.] c= the carrier of I[01] by A4, BORSUK_1:40, XXREAL_1:34; ::_thesis: verum
end;

theorem Th11: :: BORSUK_4:11
for a, b being real number st a <> b holds
Cl ].a,b.] = [.a,b.]
proof
let a, b be real number ; ::_thesis: ( a <> b implies Cl ].a,b.] = [.a,b.] )
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 ; ::_thesis: Cl ].a,b.] = [.a,b.]
then  [.a,b.] c= Cl ].a,b.] by A2, JORDAN5A:26;
hence  Cl ].a,b.] = [.a,b.] by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th12: :: BORSUK_4:12
for a, b being real number st a <> b holds
Cl [.a,b.[ = [.a,b.]
proof
let a, b be real number ; ::_thesis: ( a <> b implies Cl [.a,b.[ = [.a,b.] )
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 ; ::_thesis: Cl [.a,b.[ = [.a,b.]
then  [.a,b.] c= Cl [.a,b.[ by A2, JORDAN5A:26;
hence  Cl [.a,b.[ = [.a,b.] by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: BORSUK_4:13
for A being Subset of I[01]
for a, b being real number st a < b & A = ].a,b.[ holds
Cl A = [.a,b.]
proof
let A be Subset of I[01]; ::_thesis: for a, b being real number st a < b & A = ].a,b.[ holds
Cl A = [.a,b.]
let a, b be real number ; ::_thesis: ( a < b & A = ].a,b.[ implies Cl A = [.a,b.] )
assume that
A1: a < b and
A2: A = ].a,b.[ ; ::_thesis: Cl 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, Th8, XBOOLE_1:28 ;
hence  Cl A = [.a,b.] ; ::_thesis: verum
end;

theorem Th14: :: BORSUK_4:14
for A being Subset of I[01]
for a, b being real number st a < b & A = ].a,b.] holds
Cl A = [.a,b.]
proof
let A be Subset of I[01]; ::_thesis: for a, b being real number st a < b & A = ].a,b.] holds
Cl A = [.a,b.]
let a, b be real number ; ::_thesis: ( a < b & A = ].a,b.] implies Cl A = [.a,b.] )
assume that
A1: a < b and
A2: A = ].a,b.] ; ::_thesis: Cl A = [.a,b.]
reconsider A1 = ].a,b.] as Subset of R^1 by TOPMETR:17;
A3: Cl ].a,b.] = [.a,b.] by A1, Th11;
Cl A = (Cl A1) /\ ([#] I[01]) by A2, PRE_TOPC:17
.= [.a,b.] /\ ([#] I[01]) by A3, JORDAN5A:24
.= [.a,b.] by A1, A2, Th9, XBOOLE_1:28 ;
hence  Cl A = [.a,b.] ; ::_thesis: verum
end;

theorem Th15: :: BORSUK_4:15
for A being Subset of I[01]
for a, b being real number st a < b & A = [.a,b.[ holds
Cl A = [.a,b.]
proof
let A be Subset of I[01]; ::_thesis: for a, b being real number st a < b & A = [.a,b.[ holds
Cl A = [.a,b.]
let a, b be real number ; ::_thesis: ( a < b & A = [.a,b.[ implies Cl A = [.a,b.] )
assume that
A1: a < b and
A2: A = [.a,b.[ ; ::_thesis: Cl A = [.a,b.]
reconsider A1 = [.a,b.[ as Subset of R^1 by TOPMETR:17;
A3: Cl [.a,b.[ = [.a,b.] by A1, Th12;
Cl A = (Cl A1) /\ ([#] I[01]) by A2, PRE_TOPC:17
.= [.a,b.] /\ ([#] I[01]) by A3, JORDAN5A:24
.= [.a,b.] by A1, A2, Th10, XBOOLE_1:28 ;
hence  Cl A = [.a,b.] ; ::_thesis: verum
end;

theorem Th16: :: BORSUK_4:16
for A being Subset of I[01]
for a, b being real number st a <= b & A = [.a,b.] holds
( 0 <= a & b <= 1 )
proof
let A be Subset of I[01]; ::_thesis: for a, b being real number st a <= b & A = [.a,b.] holds
( 0 <= a & b <= 1 )
let a, b be real number ; ::_thesis: ( a <= b & A = [.a,b.] implies ( 0 <= a & b <= 1 ) )
assume that
A1: a <= b and
A2: A = [.a,b.] ; ::_thesis: ( 0 <= a & b <= 1 )
A3: b in A by A1, A2, XXREAL_1:1;
 a in A by A1, A2, XXREAL_1:1;
hence  ( 0 <= a & b <= 1 ) by A3, BORSUK_1:43; ::_thesis: verum
end;

theorem Th17: :: BORSUK_4:17
for A, B being Subset of I[01]
for a, b, c being real number 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]; ::_thesis: for a, b, c being real number st a < b & b < c & A = [.a,b.[ & B = ].b,c.] holds
A,B are_separated
let a, b, c be real number ; ::_thesis: ( a < b & b < c & A = [.a,b.[ & B = ].b,c.] implies A,B are_separated )
assume that
A1: a < b and
A2: b < c and
A3: A = [.a,b.[ and
A4: B = ].b,c.] ; ::_thesis: A,B are_separated
 Cl A = [.a,b.] by A1, A3, Th15;
hence  Cl A misses B by A4, XXREAL_1:90; :: according to CONNSP_1:def_1 ::_thesis: A misses Cl B
 Cl B = [.b,c.] by A2, A4, Th14;
hence  A misses Cl B by A3, XXREAL_1:95; ::_thesis: verum
end;

theorem :: BORSUK_4:18
for p1, p2 being Point of I[01] holds [.p1,p2.] is Subset of I[01] by BORSUK_1:40, XXREAL_2:def_12;

theorem Th19: :: BORSUK_4:19
for a, b being Point of I[01] holds ].a,b.[ is Subset of I[01]
proof
let a, b be Point of I[01]; ::_thesis: ].a,b.[ is Subset 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  ].a,b.[ is Subset of I[01] by A1, XBOOLE_1:1; ::_thesis: verum
end;

begin

theorem :: BORSUK_4:20
for p being real number holds {p} is non empty closed_interval Subset of REAL
proof
let p be real number ; ::_thesis: {p} is non empty closed_interval Subset of REAL
A1: {p} = [.p,p.] by XXREAL_1:17;
 p is Real by XREAL_0:def_1;
hence  {p} is non empty closed_interval Subset of REAL by A1, MEASURE5:14; ::_thesis: verum
end;

theorem Th21: :: BORSUK_4:21
for A being non empty connected Subset of I[01]
for a, b, c being 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]; ::_thesis: for a, b, c being Point of I[01] st a <= b & b <= c & a in A & c in A holds
b in A
let a, b, c be Point of I[01]; ::_thesis: ( a <= b & b <= c & a in A & c in A implies b in A )
assume that
A1: a <= b and
A2: b <= c and
A3: a in A and
A4: c in A ; ::_thesis: b in A
percases ( a = b or b = c or ( a < b & b < c & a in A & c in A ) ) by A1, A2, A3, A4, XXREAL_0:1;
suppose ( a = b or b = c ) ; ::_thesis: b in A
hence  b in A by A3, A4; ::_thesis: verum
end;
supposeA5: ( a < b & b < c & a in A & c in A ) ; ::_thesis: b 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 ; ::_thesis: contradiction
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__::_thesis:_contradiction
percases ( A c= B or A c= C ) by A5, A8, A10, A13, Th17, CONNSP_1:16;
suppose A c= B ; ::_thesis: contradiction
hence  contradiction by A5, XXREAL_1:3; ::_thesis: verum
end;
suppose A c= C ; ::_thesis: contradiction
hence  contradiction by A5, XXREAL_1:2; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;

theorem Th22: :: BORSUK_4:22
for A being non empty connected Subset of I[01]
for a, b being real number st a in A & b in A holds
[.a,b.] c= A
proof
let A be non empty connected Subset of I[01]; ::_thesis: for a, b being real number st a in A & b in A holds
[.a,b.] c= A
let a, b be real number ; ::_thesis: ( a in A & b in A implies [.a,b.] c= A )
assume that
A1: a in A and
A2: b in A ; ::_thesis: [.a,b.] c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.a,b.] or x in A )
assume  x in [.a,b.] ; ::_thesis: x in A
then  x in  {  y where y is Real : ( a <= y & y <= b )  }  by RCOMP_1:def_1;
then consider z being 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 = z as Point of I[01] by A6, BORSUK_1:43;
 z in A by A1, A2, A4, A5, Th21;
hence  x in A by A3; ::_thesis: verum
end;

theorem Th23: :: BORSUK_4:23
for a, b being real number
for A being Subset of I[01] st A = [.a,b.] holds
A is closed
proof
let a, b be real number ; ::_thesis: for A being Subset of I[01] st A = [.a,b.] holds
A is closed
let A be Subset of I[01]; ::_thesis: ( A = [.a,b.] implies A is closed )
assume A1: A = [.a,b.] ; ::_thesis: A is closed
percases ( a <= b or a > b ) ;
supposeA2: a <= b ; ::_thesis: A is closed
then A3: b <= 1 by A1, Th16;
 0 <= a by A1, A2, Th16;
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  A is closed by A1, A2, TOPMETR:18, TOPMETR:20; ::_thesis: verum
end;
suppose a > b ; ::_thesis: A is closed
then  A = {} I[01] by A1, XXREAL_1:29;
hence  A is closed ; ::_thesis: verum
end;
end;
end;

theorem Th24: :: BORSUK_4:24
for p1, p2 being Point of I[01] st p1 <= p2 holds
[.p1,p2.] is non empty connected compact Subset of I[01]
proof
let p1, p2 be Point of I[01]; ::_thesis: ( p1 <= p2 implies [.p1,p2.] is non empty connected compact Subset of I[01] )
A1: p2 <= 1 by BORSUK_1:43;
set S = [.p1,p2.];
reconsider S = [.p1,p2.] as Subset of I[01] by BORSUK_1:40, XXREAL_2:def_12;
assume A2: p1 <= p2 ; ::_thesis: [.p1,p2.] is non empty connected compact Subset of I[01]
then A3: Closed-Interval-TSpace (p1,p2) is connected by TREAL_1:20;
A4: S is closed by Th23;
 0 <= p1 by BORSUK_1:43;
then  I[01] | S = Closed-Interval-TSpace (p1,p2) by A2, A1, TOPMETR:24;
hence  [.p1,p2.] is non empty connected compact Subset of I[01] by A4, A3, COMPTS_1:8, CONNSP_1:def_3; ::_thesis: verum
end;

theorem Th25: :: BORSUK_4:25
for X being Subset of I[01]
for X9 being Subset of REAL st X9 = X holds
( X9 is bounded_above & X9 is bounded_below )
proof
let X be Subset of I[01]; ::_thesis: for X9 being Subset of REAL st X9 = X holds
( X9 is bounded_above & X9 is bounded_below )
let X9 be Subset of REAL; ::_thesis: ( X9 = X implies ( X9 is bounded_above & X9 is bounded_below ) )
assume A1: X9 = X ; ::_thesis: ( X9 is bounded_above & X9 is bounded_below )
then  for r being ext-real number 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; ::_thesis: X9 is bounded_below
 for r being ext-real number st r in X9 holds
0 <= r by A1, BORSUK_1:43;
then  0 is LowerBound of X9 by XXREAL_2:def_2;
hence  X9 is bounded_below by XXREAL_2:def_9; ::_thesis: verum
end;

theorem Th26: :: BORSUK_4:26
for X being Subset of I[01]
for X9 being Subset of REAL
for x being real number st x in X9 & X9 = X holds
( lower_bound X9 <= x & x <= upper_bound X9 )
proof
let X be Subset of I[01]; ::_thesis: for X9 being Subset of REAL
for x being real number st x in X9 & X9 = X holds
( lower_bound X9 <= x & x <= upper_bound X9 )
let X9 be Subset of REAL; ::_thesis: for x being real number st x in X9 & X9 = X holds
( lower_bound X9 <= x & x <= upper_bound X9 )
let x be real number ; ::_thesis: ( x in X9 & X9 = X implies ( lower_bound X9 <= x & x <= upper_bound X9 ) )
assume that
A1: x in X9 and
A2: X9 = X ; ::_thesis: ( lower_bound X9 <= x & x <= upper_bound X9 )
 ( X9 is bounded_above & X9 is bounded_below ) by A2, Th25;
hence  ( lower_bound X9 <= x & x <= upper_bound X9 ) by A1, SEQ_4:def_1, SEQ_4:def_2; ::_thesis: verum
end;

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

theorem Th27: :: BORSUK_4:27
for A being Subset of REAL
for B being 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; ::_thesis: for B being Subset of I[01] st A = B holds
( A is closed iff B is closed )
let B be Subset of I[01]; ::_thesis: ( A = B implies ( A is closed iff B is closed ) )
assume A1: A = B ; ::_thesis: ( A is closed iff B is closed )
 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  ::_thesis: ( B is closed implies A is closed )
assume  A is closed ; ::_thesis: B 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; ::_thesis: verum
end;
assume A3: B is closed ; ::_thesis: A 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  A is closed by A3, JORDAN5A:23; ::_thesis: verum
end;

theorem Th28: :: BORSUK_4:28
for C being 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; ::_thesis: lower_bound C <= upper_bound C
set c = the Element of C;
A1: the Element of C <= upper_bound C by INTEGRA2:1;
 lower_bound C <= the Element of C by INTEGRA2:1;
hence  lower_bound C <= upper_bound C by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem Th29: :: BORSUK_4:29
for C being non empty connected compact Subset of I[01]
for C9 being 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 connected compact Subset of I[01]; ::_thesis: for C9 being Subset of REAL st C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 holds
[.(lower_bound C9),(upper_bound C9).] = C9
let C9 be Subset of REAL; ::_thesis: ( C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 implies [.(lower_bound C9),(upper_bound C9).] = C9 )
assume that
A1: C = C9 and
A2: [.(lower_bound C9),(upper_bound C9).] c= C9 ; ::_thesis: [.(lower_bound C9),(upper_bound C9).] = C9
assume  [.(lower_bound C9),(upper_bound C9).] <> C9 ; ::_thesis: contradiction
then  not C9 c= [.(lower_bound C9),(upper_bound C9).] by A2, XBOOLE_0:def_10;
then consider c being set  such that
A3: c in C9 and
A4: not c in [.(lower_bound C9),(upper_bound C9).] by TARSKI:def_3;
reconsider c = c as real number by A3;
A5: c <= upper_bound C9 by A1, A3, Th26;
 lower_bound C9 <= c by A1, A3, Th26;
hence  contradiction by A4, A5, XXREAL_1:1; ::_thesis: verum
end;

theorem Th30: :: BORSUK_4:30
for C being non empty connected compact Subset of I[01] holds C is non empty closed_interval Subset of REAL
proof
let C be non empty connected compact Subset of I[01]; ::_thesis: C is non empty closed_interval Subset of REAL
reconsider C9 = C as Subset of REAL by BORSUK_1:40, XBOOLE_1:1;
 ( C9 is bounded_below & C9 is bounded_above ) by Th25;
then A1: lower_bound C9 <= upper_bound C9 by SEQ_4:11;
A2: C9 is closed by Th27;
then A3: upper_bound C9 in C9 by Th25, RCOMP_1:12;
 lower_bound C9 in C9 by A2, Th25, RCOMP_1:13;
then  [.(lower_bound C9),(upper_bound C9).] = C9 by A3, Th22, Th29;
hence  C is non empty closed_interval Subset of REAL by A1, MEASURE5:14; ::_thesis: verum
end;

theorem Th31: :: BORSUK_4:31
for C being non empty connected compact Subset of I[01] ex p1, p2 being Point of I[01] st
( p1 <= p2 & C = [.p1,p2.] )
proof
let C be non empty connected compact Subset of I[01]; ::_thesis: ex p1, p2 being Point of I[01] st
( p1 <= p2 & C = [.p1,p2.] )
reconsider C9 = C as non empty closed_interval Subset of REAL by Th30;
A1: C9 = [.(lower_bound C9),(upper_bound C9).] by INTEGRA1:4;
A2: lower_bound C9 <= upper_bound C9 by Th28;
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 ; ::_thesis: ex p2 being Point of I[01] st
( p1 <= p2 & C = [.p1,p2.] )
take  p2 ; ::_thesis: ( p1 <= p2 & C = [.p1,p2.] )
thus  p1 <= p2 by Th28; ::_thesis: C = [.p1,p2.]
thus  C = [.p1,p2.] by INTEGRA1:4; ::_thesis: verum
end;

begin

definition
func I(01)  ->  strict SubSpace of I[01]  means :Def1: :: BORSUK_4:def 1
 the carrier of it = ].0,1.[;
existence
 ex b1 being strict SubSpace of I[01] st the carrier of b1 = ].0,1.[
proof
reconsider E = ].0,1.[ as Subset of I[01] by BORSUK_1:40, XXREAL_1:25;
take  I[01] | E ; ::_thesis: the carrier of (I[01] | E) = ].0,1.[
thus  the carrier of (I[01] | E) = ].0,1.[ by PRE_TOPC:8; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict SubSpace of I[01] st the carrier of b1 = ].0,1.[ & the carrier of b2 = ].0,1.[ holds
b1 = b2 by TSEP_1:5;
end;

:: deftheorem Def1 defines I(01) BORSUK_4:def_1_:_
 for b1 being strict SubSpace of I[01] holds
( b1 = I(01) iff the carrier of b1 = ].0,1.[ );

registration
cluster I(01)  ->  non empty strict ;
coherence
 not I(01) is empty
proof
 the carrier of I(01) = ].0,1.[ by Def1;
hence  not the carrier of I(01) is empty by XXREAL_1:33; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

theorem :: BORSUK_4:32
for A being 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 Th33: :: BORSUK_4:33
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  the carrier of I(01) = the carrier of I[01] \ {0,1} by A1, BORSUK_1:40, XBOOLE_1:88, XXREAL_1:86; ::_thesis: verum
end;

registration
cluster I(01)  ->  strict open ;
coherence
 I(01) is open by Th33, JORDAN6:34, TSEP_1:def_1;
end;

theorem :: BORSUK_4:34
I(01) is open ;

theorem Th35: :: BORSUK_4:35
for r being real number holds
( r in the carrier of I(01) iff ( 0 < r & r < 1 ) )
proof
let r be real number ; ::_thesis: ( r in the carrier of I(01) iff ( 0 < r & r < 1 ) )
hereby  ::_thesis: ( 0 < r & r < 1 implies r in the carrier of I(01) )
assume  r in the carrier of I(01) ; ::_thesis: ( 0 < r & r < 1 )
then  r in ].0,1.[ by Def1;
hence  ( 0 < r & r < 1 ) by XXREAL_1:4; ::_thesis: verum
end;
assume that
A1: 0 < r and
A2: r < 1 ; ::_thesis: r in the carrier of I(01)
 r in ].0,1.[ by A1, A2, XXREAL_1:4;
hence  r in the carrier of I(01) by Def1; ::_thesis: verum
end;

theorem Th36: :: BORSUK_4:36
for a, b being Point of I[01] st a < b & b <> 1 holds
].a,b.] is non empty Subset of I(01)
proof
let a, b be Point of I[01]; ::_thesis: ( a < b & b <> 1 implies ].a,b.] is non empty Subset of I(01) )
assume that
A1: a < b and
A2: b <> 1 ; ::_thesis: ].a,b.] is non empty Subset of I(01)
 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].a,b.] or x in the carrier of I(01) )
assume  x in ].a,b.] ; ::_thesis: x in the carrier of I(01)
then  x in  {  r where r is Real : ( a < r & r <= b )  }  by RCOMP_1:def_8;
then consider r being 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  x in the carrier of I(01) by A4, A7, Th35; ::_thesis: verum
end;
hence  ].a,b.] is non empty Subset of I(01) by A1, XXREAL_1:2; ::_thesis: verum
end;

theorem Th37: :: BORSUK_4:37
for a, b being Point of I[01] st a < b & a <> 0 holds
[.a,b.[ is non empty Subset of I(01)
proof
let a, b be Point of I[01]; ::_thesis: ( a < b & a <> 0 implies [.a,b.[ is non empty Subset of I(01) )
assume that
A1: a < b and
A2: a <> 0 ; ::_thesis: [.a,b.[ is non empty Subset of I(01)
A3: b <= 1 by BORSUK_1:43;
 [.a,b.[ c= the carrier of I(01)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.a,b.[ or x in the carrier of I(01) )
assume  x in [.a,b.[ ; ::_thesis: x in the carrier of I(01)
then  x in  {  r where r is Real : ( a <= r & r < b )  }  by RCOMP_1:def_7;
then consider r being 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  x in the carrier of I(01) by A4, A7, Th35; ::_thesis: verum
end;
hence  [.a,b.[ is non empty Subset of I(01) by A1, XXREAL_1:3; ::_thesis: verum
end;

theorem :: BORSUK_4:38
for D being Simple_closed_curve holds (TOP-REAL 2) | R^2-unit_square,(TOP-REAL 2) | D are_homeomorphic
proof
let D be Simple_closed_curve; ::_thesis: (TOP-REAL 2) | R^2-unit_square,(TOP-REAL 2) | D are_homeomorphic
 ex f being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | D) st f is being_homeomorphism by TOPREAL2:def_1;
hence  (TOP-REAL 2) | R^2-unit_square,(TOP-REAL 2) | D are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum
end;

theorem :: BORSUK_4:39
for n being Element of NAT
for D being non empty Subset of (TOP-REAL n)
for p1, p2 being 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 ; ::_thesis: for D being non empty Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st D is_an_arc_of p1,p2 holds
I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic
let D be non empty Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st D is_an_arc_of p1,p2 holds
I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( D is_an_arc_of p1,p2 implies I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic )
assume A1: D is_an_arc_of p1,p2 ; ::_thesis: I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic
then consider f being 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 & f is 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 Th33, 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 = (f ") | D1 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 = f | the carrier of I(01) as Function of (I[01] | K0),((TOP-REAL n) | D) by FUNCT_2:32;
A16: dom (f | the carrier of I(01)) = 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 " by A9, TOPS_2:def_4;
A18: rng (f | the carrier of I(01)) = f .: the carrier of I(01) by RELAT_1:115;
then A19: rng (f | the carrier of I(01)) = the carrier of ((TOP-REAL n) | (D \ {p1,p2})) by A10, PRE_TOPC:8;
then reconsider fD = f | the carrier of I(01) 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 " 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  I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum
end;

theorem Th40: :: BORSUK_4:40
for n being Element of NAT
for D being Subset of (TOP-REAL n)
for p1, p2 being 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 ; ::_thesis: for D being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st D is_an_arc_of p1,p2 holds
I[01] ,(TOP-REAL n) | D are_homeomorphic
let D be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st D is_an_arc_of p1,p2 holds
I[01] ,(TOP-REAL n) | D are_homeomorphic
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( D is_an_arc_of p1,p2 implies I[01] ,(TOP-REAL n) | D are_homeomorphic )
assume  D is_an_arc_of p1,p2 ; ::_thesis: I[01] ,(TOP-REAL n) | D are_homeomorphic
then  ex f being Function of I[01],((TOP-REAL n) | D) st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by TOPREAL1:def_1;
hence  I[01] ,(TOP-REAL n) | D are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum
end;

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

theorem Th42: :: BORSUK_4:42
for E being Subset of I(01) st ex p1, p2 being 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); ::_thesis: ( ex p1, p2 being Point of I[01] st
( p1 < p2 & E = [.p1,p2.] ) implies I[01] ,I(01) | E are_homeomorphic )
given p1, p2 being Point of I[01] such that A1: p1 < p2 and
A2: E = [.p1,p2.] ; ::_thesis: I[01] ,I(01) | E are_homeomorphic
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) (#)));
 L[01] (((#) (p1,p2)),((p1,p2) (#))) is being_homeomorphism by A1, TREAL_1:17;
hence  I[01] ,I(01) | E are_homeomorphic by A4, TOPMETR:20, T_0TOPSP:def_1; ::_thesis: verum
end;

theorem Th43: :: BORSUK_4:43
for n being Element of NAT
for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b holds
ex E being non empty Subset of I[01] ex f being 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 ; ::_thesis: for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b holds
ex E being non empty Subset of I[01] ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is being_homeomorphism & f . a = p & f . b = q )
let A be Subset of (TOP-REAL n); ::_thesis: for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b holds
ex E being non empty Subset of I[01] ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is being_homeomorphism & f . a = p & f . b = q )
let p, q be Point of (TOP-REAL n); ::_thesis: for a, b being Point of I[01] st A is_an_arc_of p,q & a < b holds
ex E being non empty Subset of I[01] ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is being_homeomorphism & f . a = p & f . b = q )
let a, b be Point of I[01]; ::_thesis: ( A is_an_arc_of p,q & a < b implies ex E being non empty Subset of I[01] ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is being_homeomorphism & f . a = p & f . b = q ) )
assume that
A2: A is_an_arc_of p,q and
A3: a < b ; ::_thesis: ex E being non empty Subset of I[01] ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is being_homeomorphism & f . a = p & f . b = q )
reconsider E = [.a,b.] as non empty Subset of I[01] by A3, Th24;
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 ; ::_thesis: ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is being_homeomorphism & f . a = p & f . b = q )
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 being 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 = f * e as Function of (I[01] | E),((TOP-REAL n) | A) ;
take  g ; ::_thesis: ( E = [.a,b.] & g is being_homeomorphism & g . a = p & g . b = q )
thus  E = [.a,b.] ; ::_thesis: ( g is being_homeomorphism & g . a = p & g . b = q )
 e is being_homeomorphism by A3, A5, TOPMETR:20, TREAL_1:17;
hence  g is being_homeomorphism by A7, TOPS_2:57; ::_thesis: ( g . a = p & g . b = q )
 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 ;
::_thesis: g . b = q
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 ;
::_thesis: verum
end;

theorem Th44: :: BORSUK_4:44
for A being TopSpace
for B being non empty TopSpace
for f being Function of A,B
for C being TopSpace
for X being Subset of A st f is continuous & C is SubSpace of B holds
for h being Function of (A | X),C st h = f | X holds
h is continuous
proof
let A be TopSpace; ::_thesis: for B being non empty TopSpace
for f being Function of A,B
for C being TopSpace
for X being Subset of A st f is continuous & C is SubSpace of B holds
for h being Function of (A | X),C st h = f | X holds
h is continuous
let B be non empty TopSpace; ::_thesis: for f being Function of A,B
for C being TopSpace
for X being Subset of A st f is continuous & C is SubSpace of B holds
for h being Function of (A | X),C st h = f | X holds
h is continuous
let f be Function of A,B; ::_thesis: for C being TopSpace
for X being Subset of A st f is continuous & C is SubSpace of B holds
for h being Function of (A | X),C st h = f | X holds
h is continuous
let C be TopSpace; ::_thesis: for X being Subset of A st f is continuous & C is SubSpace of B holds
for h being Function of (A | X),C st h = f | X holds
h is continuous
let X be Subset of A; ::_thesis: ( f is continuous & C is SubSpace of B implies for h being Function of (A | X),C st h = f | X holds
h is continuous )
assume that
A1: f is continuous and
A2: C is SubSpace of B ; ::_thesis: for h being Function of (A | X),C st h = f | X holds
h is continuous
 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; ::_thesis: ( h = f | X implies h is continuous )
assume A3: h = f | X ; ::_thesis: h is continuous
 g is continuous by A1, TOPMETR:7;
hence  h is continuous by A2, A3, PRE_TOPC:27; ::_thesis: verum
end;

theorem Th45: :: BORSUK_4:45
for X being Subset of I[01]
for a, b being Point of I[01] st X = ].a,b.[ holds
X is open
proof
let X be Subset of I[01]; ::_thesis: for a, b being Point of I[01] st X = ].a,b.[ holds
X is open
let a, b be Point of I[01]; ::_thesis: ( X = ].a,b.[ implies X is open )
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 Th23;
A4: A is closed by Th23;
assume  X = ].a,b.[ ; ::_thesis: X is open
then  X = (A \/ B) ` by A1, A2, BORSUK_1:40, XXREAL_1:200;
hence  X is open by A4, A3; ::_thesis: verum
end;

theorem Th46: :: BORSUK_4:46
for X being Subset of I(01)
for a, b being Point of I[01] st X = ].a,b.[ holds
X is open
proof
let X be Subset of I(01); ::_thesis: for a, b being Point of I[01] st X = ].a,b.[ holds
X is open
let a, b be Point of I[01]; ::_thesis: ( X = ].a,b.[ implies X is open )
assume A1: X = ].a,b.[ ; ::_thesis: X is open
then reconsider X9 = X as Subset of I[01] by Th19;
 X9 is open by A1, Th45;
hence  X is open by TSEP_1:17; ::_thesis: verum
end;

theorem Th47: :: BORSUK_4:47
for X being Subset of I(01)
for a being Point of I[01] st X = ].0,a.] holds
X is closed
proof
let X be Subset of I(01); ::_thesis: for a being Point of I[01] st X = ].0,a.] holds
X is closed
let a be Point of I[01]; ::_thesis: ( X = ].0,a.] implies X is closed )
assume A1: X = ].0,a.] ; ::_thesis: X is closed
percases ( 0 < a or 0 >= a ) ;
supposeA2: 0 < a ; ::_thesis: X is closed
 [#] 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, Th46;
hence  X is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
suppose 0 >= a ; ::_thesis: X is closed
then  X = {} I(01) by A1, XXREAL_1:26;
hence  X is closed ; ::_thesis: verum
end;
end;
end;

theorem Th48: :: BORSUK_4:48
for X being Subset of I(01)
for a being 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); ::_thesis: for a being Point of I[01] st X = [.a,1.[ holds
X is closed
let a be Point of I[01]; ::_thesis: ( X = [.a,1.[ implies X is closed )
assume A2: X = [.a,1.[ ; ::_thesis: X is closed
percases ( not X is empty or X is empty ) ;
supposeA3: not X is empty ; ::_thesis: X is closed
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, Th46;
hence  X is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
suppose X is empty ; ::_thesis: X is closed
hence  X is closed ; ::_thesis: verum
end;
end;
end;

theorem Th49: :: BORSUK_4:49
for n being Element of NAT
for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & b <> 1 holds
ex E being non empty Subset of I(01) ex f being 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 ; ::_thesis: for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & b <> 1 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {p})) st
( E = ].a,b.] & f is being_homeomorphism & f . b = q )
let A be Subset of (TOP-REAL n); ::_thesis: for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & b <> 1 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {p})) st
( E = ].a,b.] & f is being_homeomorphism & f . b = q )
let p, q be Point of (TOP-REAL n); ::_thesis: for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & b <> 1 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {p})) st
( E = ].a,b.] & f is being_homeomorphism & f . b = q )
let a, b be Point of I[01]; ::_thesis: ( A is_an_arc_of p,q & a < b & b <> 1 implies ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {p})) st
( E = ].a,b.] & f is being_homeomorphism & f . b = q ) )
assume that
A1: A is_an_arc_of p,q and
A2: a < b and
A3: b <> 1 ; ::_thesis: ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {p})) st
( E = ].a,b.] & f is being_homeomorphism & f . b = q )
reconsider B = A as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1;
consider F being non empty Subset of I[01], s being 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, Th43;
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, Th36;
set X = E;
A10: I(01) | E is SubSpace of I[01] by TSEP_1:7;
set sX = s | E;
A11: ( s is continuous & s is 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) | E) c= the carrier of (I[01] | F) by A15, PRE_TOPC:8;
then A17: I(01) | E 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 (s | E) = E by A4, A8, RELAT_1:62, XXREAL_1:23
.= [#] (I(01) | E) 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;
 E = F \ {a} by A2, A4, XXREAL_1:134;
then A22: s .: E = (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 (s | E) by RELAT_1:115;
 rng (s | E) = the carrier of ((TOP-REAL n) | (A \ {p})) by A22, RELAT_1:115;
then reconsider sX = s | E 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 E by A2, XXREAL_1:2;
then A26: sX . b = q by A7, FUNCT_1:49;
 the carrier of (I(01) | E) = E by PRE_TOPC:8;
then  I(01) | E = (I[01] | F) | X9 by A10, A16, PRE_TOPC:8, TSEP_1:5;
then A27: sX is continuous by A11, A14, Th44;
A28: sX is one-to-one by A11, FUNCT_1:52;
then sX " = sX " by A25, TOPS_2:def_4
.= (s ") | (s .: E) 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, Th44;
then  sX is being_homeomorphism by A23, A19, A27, A28, TOPS_2:def_5;
hence  ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {p})) st
( E = ].a,b.] & f is being_homeomorphism & f . b = q ) by A26; ::_thesis: verum
end;

theorem Th50: :: BORSUK_4:50
for n being Element of NAT
for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & a <> 0 holds
ex E being non empty Subset of I(01) ex f being 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 ; ::_thesis: for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & a <> 0 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is being_homeomorphism & f . a = p )
let A be Subset of (TOP-REAL n); ::_thesis: for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & a <> 0 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is being_homeomorphism & f . a = p )
let p, q be Point of (TOP-REAL n); ::_thesis: for a, b being Point of I[01] st A is_an_arc_of p,q & a < b & a <> 0 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is being_homeomorphism & f . a = p )
let a, b be Point of I[01]; ::_thesis: ( A is_an_arc_of p,q & a < b & a <> 0 implies ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is being_homeomorphism & f . a = p ) )
assume that
A1: A is_an_arc_of p,q and
A2: a < b and
A3: a <> 0 ; ::_thesis: ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is being_homeomorphism & f . a = p )
reconsider B = A as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1;
consider F being non empty Subset of I[01], s being 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, Th43;
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, Th37;
set X = E;
A10: I(01) | E is SubSpace of I[01] by TSEP_1:7;
set sX = s | E;
A11: ( s is continuous & s is 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) | E) c= the carrier of (I[01] | F) by A15, PRE_TOPC:8;
then A17: I(01) | E 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 (s | E) = E by A4, A8, RELAT_1:62, XXREAL_1:24
.= [#] (I(01) | E) 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;
 E = F \ {b} by A2, A4, XXREAL_1:135;
then A22: s .: E = (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 (s | E) by RELAT_1:115;
 rng (s | E) = the carrier of ((TOP-REAL n) | (A \ {q})) by A22, RELAT_1:115;
then reconsider sX = s | E 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 E by A2, XXREAL_1:3;
then A26: sX . a = p by A6, FUNCT_1:49;
 the carrier of (I(01) | E) = E by PRE_TOPC:8;
then  I(01) | E = (I[01] | F) | X9 by A10, A16, PRE_TOPC:8, TSEP_1:5;
then A27: sX is continuous by A11, A14, Th44;
A28: sX is one-to-one by A11, FUNCT_1:52;
then sX " = sX " by A24, TOPS_2:def_4
.= (s ") | (s .: E) 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, Th44;
then  sX is being_homeomorphism by A23, A19, A27, A28, TOPS_2:def_5;
hence  ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ & f is being_homeomorphism & f . a = p ) by A26; ::_thesis: verum
end;

theorem Th51: :: BORSUK_4:51
for n being Element of NAT
for A, B being Subset of (TOP-REAL n)
for p, q being 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 ; ::_thesis: for A, B being Subset of (TOP-REAL n)
for p, q being 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
let A, B be Subset of (TOP-REAL n); ::_thesis: for p, q being 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
let p, q be Point of (TOP-REAL n); ::_thesis: ( A is_an_arc_of p,q & B is_an_arc_of q,p & A /\ B = {p,q} & p <> q implies I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic )
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 ; ::_thesis: I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic
consider E2 being non empty Subset of I(01), ty being 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, Th50;
consider E1 being non empty Subset of I(01), sx being 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, Th49;
set T1 = I(01) | E1;
set T2 = I(01) | E2;
set T = I(01) ;
set S = (TOP-REAL n) | ((A \ {p}) \/ (B \ {p}));
set U1 = (TOP-REAL n) | (A \ {p});
set U2 = (TOP-REAL n) | (B \ {p});
A11: not A \ {p} is empty by A1, Th6;
then reconsider S = (TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) as non empty SubSpace of TOP-REAL n ;
 not B \ {p} is empty by A2, Th6, JORDAN5B:14;
then reconsider U1 = (TOP-REAL n) | (A \ {p}), U2 = (TOP-REAL n) | (B \ {p}) 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 (I(01) | E2),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 = [#] (I(01) | E1), F2 = [#] (I(01) | E2) as non empty Subset of I(01) 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 (I(01) | E1),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, Th48;
A28: F1 = ].0,(1 / 2).] by A8, PRE_TOPC:def_5;
then A29: ([#] (I(01) | E1)) \/ ([#] (I(01) | E2)) = ].0,1.[ by A16, XXREAL_1:172
.= [#] I(01) by Def1 ;
A30: ([#] (I(01) | E1)) /\ ([#] (I(01) | E2)) = {(1 / 2)} by A28, A16, XXREAL_1:138;
A31: for d being set st d in ([#] (I(01) | E1)) /\ ([#] (I(01) | E2)) holds
sx . d = ty . d
proof
let d be set ; ::_thesis: ( d in ([#] (I(01) | E1)) /\ ([#] (I(01) | E2)) implies sx . d = ty . d )
assume  d in ([#] (I(01) | E1)) /\ ([#] (I(01) | E2)) ; ::_thesis: sx . d = ty . d
then  d = b by A30, TARSKI:def_1;
hence  sx . d = ty . d by A10, A7; ::_thesis: verum
end;
 F1 is closed by A26, A28, Th47;
then consider F being Function of I(01),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 (I(01) | E2) c= the carrier of I(01) by BORSUK_1:1;
then reconsider g = ty " as Function of U2,I(01) by FUNCT_2:7;
 the carrier of (I(01) | E1) c= the carrier of I(01) by BORSUK_1:1;
then reconsider f = sx " as Function of U1,I(01) by FUNCT_2:7;
A36: dom ty9 = [#] (I(01) | E2) 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  V2 is closed by A40, PRE_TOPC:13; ::_thesis: verum
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  V1 is closed by A45, PRE_TOPC:13; ::_thesis: verum
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 " by A21, TOPS_2:def_4;
A53: dom sx9 = [#] (I(01) | E1) 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 set ; :: according to PARTFUN1:def_4 ::_thesis: ( not t in (dom sx9) /\ (dom ty9) or sx9 . t = ty9 . t )
assume  t in (dom sx9) /\ (dom ty9) ; ::_thesis: sx9 . t = ty9 . t
then  t = b by A54, TARSKI:def_1;
hence  sx9 . t = ty9 . t by A10, A7; ::_thesis: verum
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 " by A56, TOPS_2:def_4;
A59: for r being set st r in ([#] U1) /\ ([#] U2) holds
f . r = g . r
proof
let r be set ; ::_thesis: ( r in ([#] U1) /\ ([#] U2) implies f . r = g . r )
 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) ; ::_thesis: f . r = g . r
then  r = q by A10, A22, A19, A24, TARSKI:def_1;
hence  f . r = g . r by A7, A51, A52, A60, A61, FUNCT_1:34; ::_thesis: verum
end;
 ([#] U1) \/ ([#] U2) = [#] S by A37, A34, PRE_TOPC:def_5;
then A62: ex h being Function of S,I(01) 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, Th4;
then  F " = F " by A63, TOPS_2:def_4;
then  F " = (sx ") +* (ty ") by A10, A7, A32, A57, A51, A54, A24, A58, A52, Th5;
then  F is being_homeomorphism by A33, A38, A64, A55, A62, TOPS_2:def_5;
hence  I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum
end;

theorem Th52: :: BORSUK_4:52
for D being Simple_closed_curve
for p being 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; ::_thesis: for p being Point of (TOP-REAL 2) st p in D holds
(TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic
let p be Point of (TOP-REAL 2); ::_thesis: ( p in D implies (TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic )
consider q being Point of (TOP-REAL 2) such that
A1: q in D and
A2: p <> q by Th3;
 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 ; ::_thesis: (TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic
then consider P1, P2 being 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, Th51;
hence  (TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic ; ::_thesis: verum
end;

theorem :: BORSUK_4:53
for D being Simple_closed_curve
for p, q being 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; ::_thesis: for p, q being 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
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in D & q in D implies (TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic )
assume that
A1: p in D and
A2: q in D ; ::_thesis: (TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic
percases ( p = q or p <> q ) ;
suppose p = q ; ::_thesis: (TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic
hence  (TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic ; ::_thesis: verum
end;
suppose p <> q ; ::_thesis: (TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic
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, Th52;
 (TOP-REAL 2) | Dp, I(01) are_homeomorphic by A1, Th52;
hence  (TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic by A3, BORSUK_3:3; ::_thesis: verum
end;
end;
end;

theorem Th54: :: BORSUK_4:54
for n being Element of NAT
for C being non empty Subset of (TOP-REAL n)
for E being Subset of I(01) st ex p1, p2 being Point of I[01] st
( p1 < p2 & E = [.p1,p2.] ) & I(01) | E,(TOP-REAL n) | C are_homeomorphic holds
ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2
proof
let n be Element of NAT ; ::_thesis: for C being non empty Subset of (TOP-REAL n)
for E being Subset of I(01) st ex p1, p2 being Point of I[01] st
( p1 < p2 & E = [.p1,p2.] ) & I(01) | E,(TOP-REAL n) | C are_homeomorphic holds
ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2
let C be non empty Subset of (TOP-REAL n); ::_thesis: for E being Subset of I(01) st ex p1, p2 being Point of I[01] st
( p1 < p2 & E = [.p1,p2.] ) & I(01) | E,(TOP-REAL n) | C are_homeomorphic holds
ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2
let E be Subset of I(01); ::_thesis: ( ex p1, p2 being Point of I[01] st
( p1 < p2 & E = [.p1,p2.] ) & I(01) | E,(TOP-REAL n) | C are_homeomorphic implies ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2 )
given p1, p2 being Point of I[01] such that A1: p1 < p2 and
A2: E = [.p1,p2.] ; ::_thesis: ( not I(01) | E,(TOP-REAL n) | C are_homeomorphic or ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2 )
A3: I[01] ,I(01) | E are_homeomorphic by A1, A2, Th42;
assume A4: I(01) | E,(TOP-REAL n) | C are_homeomorphic ; ::_thesis: ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2
 not E is empty by A1, A2, Th24;
then  I[01] ,(TOP-REAL n) | C are_homeomorphic by A4, A3, BORSUK_3:3;
then consider g being Function of I[01],((TOP-REAL n) | C) such that
A5: g is being_homeomorphism by T_0TOPSP:def_1;
set s1 = g . 0;
set 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 = g . 0, s2 = g . 1 as Point of (TOP-REAL n) by A6, A7;
 C is_an_arc_of s1,s2 by A5, TOPREAL1:def_1;
hence  ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2 ; ::_thesis: verum
end;

theorem Th55: :: BORSUK_4:55
for Dp being non empty Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | Dp),I(01)
for C being non empty Subset of (TOP-REAL 2) st f is being_homeomorphism & C c= Dp & ex p1, p2 being Point of I[01] st
( p1 < p2 & f .: C = [.p1,p2.] ) holds
ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2
proof
let Dp be non empty Subset of (TOP-REAL 2); ::_thesis: for f being Function of ((TOP-REAL 2) | Dp),I(01)
for C being non empty Subset of (TOP-REAL 2) st f is being_homeomorphism & C c= Dp & ex p1, p2 being Point of I[01] st
( p1 < p2 & f .: C = [.p1,p2.] ) holds
ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2
let f be Function of ((TOP-REAL 2) | Dp),I(01); ::_thesis: for C being non empty Subset of (TOP-REAL 2) st f is being_homeomorphism & C c= Dp & ex p1, p2 being Point of I[01] st
( p1 < p2 & f .: C = [.p1,p2.] ) holds
ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2
let C be non empty Subset of (TOP-REAL 2); ::_thesis: ( f is being_homeomorphism & C c= Dp & ex p1, p2 being Point of I[01] st
( p1 < p2 & f .: C = [.p1,p2.] ) implies ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2 )
assume that
A1: f is being_homeomorphism and
A2: C c= Dp ; ::_thesis: ( for p1, p2 being Point of I[01] holds
( not p1 < p2 or not f .: C = [.p1,p2.] ) or ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2 )
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 being Point of I[01] such that A5: p1 < p2 and
A6: f .: C = [.p1,p2.] ; ::_thesis: ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2
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 & f is 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: (f ") | E is Function of the carrier of (I(01) | E), the carrier of ((TOP-REAL 2) | Dp) by FUNCT_2:32;
A12: rng ((f ") | E) = (f ") .: E by RELAT_1:115
.= [#] ((TOP-REAL 2) | C) by A9, PRE_TOPC:8 ;
then reconsider g = (f ") | E 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 " by A14, TOPS_2:def_4
.= ((f ") ") | ((f ") .: E) by A13, RFUNCT_2:17
.= ((f ") ") | ((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, Th44;
 ((TOP-REAL 2) | Dp) | C9 = (TOP-REAL 2) | C by A2, PRE_TOPC:7;
then  t is continuous by A8, Th44;
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  ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2 by A5, Th54; ::_thesis: verum
end;

theorem :: BORSUK_4:56
for D being Simple_closed_curve
for C being non empty connected compact Subset of (TOP-REAL 2) holds
( not C c= D or C = D or ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
proof
let D be Simple_closed_curve; ::_thesis: for C being non empty connected compact Subset of (TOP-REAL 2) holds
( not C c= D or C = D or ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
let C be non empty connected compact Subset of (TOP-REAL 2); ::_thesis: ( not C c= D or C = D or ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
assume A1: C c= D ; ::_thesis: ( C = D or ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
assume A2: C <> D ; ::_thesis: ( ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
percases ( C is trivial or not C is trivial ) ;
suppose C is trivial ; ::_thesis: ( ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
hence  ( ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} ) by Th1; ::_thesis: verum
end;
supposeA3: not C is trivial ; ::_thesis: ( ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
 C c< D by A1, A2, XBOOLE_0:def_8;
then consider p being Point of (TOP-REAL 2) such that
A4: p in D and
A5: C c= D \ {p} by SUBSET_1:44;
consider d1, d2 being 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, Th52;
then consider f being 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 = f .: C9 as connected compact 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 being 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 = fC9 as non empty connected compact Subset of I[01] by A13, A14, COMPTS_1:2, CONNSP_1:23;
consider p1, p2 being Point of I[01] such that
A19: p1 <= p2 and
A20: fC9 = [.p1,p2.] by Th31;
A21: f . d1 in f .: C9 by A6, FUNCT_2:35;
 p1 <> p2
proof
assume  p1 = p2 ; ::_thesis: contradiction
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  contradiction by A8, A15, A17, A16, A23, FUNCT_1:def_4; ::_thesis: verum
end;
then  p1 < p2 by A19, XXREAL_0:1;
hence  ( ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} ) by A5, A9, A20, Th55; ::_thesis: verum
end;
end;
end;

begin

theorem Th57: :: BORSUK_4:57
for C being non empty compact Subset of I[01] st C c= ].0,1.[ holds
ex D being 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]; ::_thesis: ( C c= ].0,1.[ implies ex D being 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 ) )
assume A1: C c= ].0,1.[ ; ::_thesis: ex D being 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 )
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 & C9 is bounded_above ) by Th25;
then A3: lower_bound C9 <= upper_bound C9 by SEQ_4:11;
A4: C c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in D )
assume A5: x in C ; ::_thesis: x in D
then  x in the carrier of I[01] ;
then reconsider x9 = x as Real by BORSUK_1:40;
A6: x9 <= upper_bound C9 by A5, Th26;
 lower_bound C9 <= x9 by A5, Th26;
hence  x in D by A6, XXREAL_1:1; ::_thesis: verum
end;
A7: C9 is closed by Th27;
then A8: lower_bound C9 in C9 by Th25, RCOMP_1:13;
A9: upper_bound C9 in C9 by A7, Th25, RCOMP_1:12;
then A10: D is non empty connected compact Subset of I[01] by A2, A8, Th24, SEQ_4:11;
then A11: D is non empty closed_interval Subset of REAL by Th30;
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 ; ::_thesis: contradiction
then  upper_bound D >= 1 by A11, INTEGRA2:1;
hence  contradiction by A1, A9, A13, XXREAL_1:4; ::_thesis: verum
end;
A15: lower_bound C9 = lower_bound D by A3, A12, XXREAL_1:66;
A16: not 0 in D
proof
assume  0 in D ; ::_thesis: contradiction
then  lower_bound D <= 0 by A11, INTEGRA2:1;
hence  contradiction by A1, A8, A15, XXREAL_1:4; ::_thesis: verum
end;
A17: D c= ].0,1.[
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in ].0,1.[ )
assume  x in D ; ::_thesis: x in ].0,1.[
hence  x in ].0,1.[ by A10, A16, A14, BORSUK_1:40, XXREAL_1:5; ::_thesis: verum
end;
reconsider D = D as non empty closed_interval Subset of REAL by A3, MEASURE5:14;
take  D ; ::_thesis: ( C c= D & D c= ].0,1.[ & lower_bound C = lower_bound D & upper_bound C = upper_bound D )
thus  ( C c= D & D c= ].0,1.[ & lower_bound C = lower_bound D & upper_bound C = upper_bound D ) by A4, A3, A12, A17, XXREAL_1:66; ::_thesis: verum
end;

theorem Th58: :: BORSUK_4:58
for C being non empty compact Subset of I[01] st C c= ].0,1.[ holds
ex p1, p2 being 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]; ::_thesis: ( C c= ].0,1.[ implies ex p1, p2 being Point of I[01] st
( p1 <= p2 & C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ ) )
assume  C c= ].0,1.[ ; ::_thesis: ex p1, p2 being Point of I[01] st
( p1 <= p2 & C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ )
then consider D being 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 Th57;
consider p1, p2 being 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 = p1, p2 = p2 as Point of I[01] by A5, A6, BORSUK_1:40;
take  p1 ; ::_thesis: ex p2 being Point of I[01] st
( p1 <= p2 & C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ )
take  p2 ; ::_thesis: ( p1 <= p2 & C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ )
thus  p1 <= p2 by A3; ::_thesis: ( C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ )
thus  ( C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ ) by A1, A2, A4; ::_thesis: verum
end;

theorem :: BORSUK_4:59
for D being Simple_closed_curve
for C being closed Subset of (TOP-REAL 2) st C c< D holds
ex p1, p2 being Point of (TOP-REAL 2) ex B being 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; ::_thesis: for C being closed Subset of (TOP-REAL 2) st C c< D holds
ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )
let C be closed Subset of (TOP-REAL 2); ::_thesis: ( C c< D implies ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D ) )
assume A1: C c< D ; ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )
then A2: C c= D by XBOOLE_0:def_8;
A3: for C being compact Subset of (TOP-REAL 2) st not C is trivial & C c< D holds
ex p1, p2 being Point of (TOP-REAL 2) ex B being 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); ::_thesis: ( not C is trivial & C c< D implies ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D ) )
assume  not C is trivial ; ::_thesis: ( not C c< D or ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D ) )
then consider d1, d2 being 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 ; ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )
then consider p being 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, Th52;
then consider f being 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 = f .: C9 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 being 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 = fC9 as non empty compact Subset of I[01] by A18, A19, COMPTS_1:2;
consider p1, p2 being Point of I[01] such that
A22: p1 <= p2 and
A23: fC9 c= [.p1,p2.] and
A24: [.p1,p2.] c= ].0,1.[ by A20, Th58;
reconsider E = [.p1,p2.] as non empty connected compact Subset of I[01] by A22, Th24;
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 ; ::_thesis: contradiction
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  contradiction by A6, A11, A10, A12, A28, FUNCT_1:def_4; ::_thesis: verum
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 being Point of (TOP-REAL 2) such that
A30: B is_an_arc_of s1,s2 by A9, A29, A15, Th55, RELAT_1:132;
take  s1 ; ::_thesis: ex p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of s1,p2 & C c= B & B c= D )
take  s2 ; ::_thesis: ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of s1,s2 & C c= B & B c= D )
take  B ; ::_thesis: ( B is_an_arc_of s1,s2 & C c= B & B c= D )
thus  B is_an_arc_of s1,s2 by A30; ::_thesis: ( C c= B & B c= D )
 Dp c= D by XBOOLE_1:36;
hence  ( C c= B & B c= D ) by A23, A25, A15, A13, FUNCT_1:93, XBOOLE_1:1; ::_thesis: verum
end;
A31: C is compact by A2, RLTOPSP1:42, TOPREAL6:79;
percases ( C is trivial or not C is trivial ) ;
supposeA32: C is trivial ; ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )
percases ( C = {} or C <> {} ) ;
supposeA33: C = {} ; ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )
consider p, q being 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: not CC is trivial by A34, A37, ZFMISC_1:def_10;
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 ; ::_thesis: contradiction
then  D \ CC = {} by XBOOLE_1:37;
then  not {} ((TOP-REAL 2) | D) is connected by A34, A35, A36, JORDAN6:47;
hence  contradiction ; ::_thesis: verum
end;
 CC c= D by A35, A36, ZFMISC_1:32;
then  CC c< D by A40, XBOOLE_0:def_8;
then consider p1, p2 being Point of (TOP-REAL 2), B being 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 ; ::_thesis: ex p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )
take  p2 ; ::_thesis: ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )
take  B ; ::_thesis: ( B is_an_arc_of p1,p2 & C c= B & B c= D )
thus  B is_an_arc_of p1,p2 by A41; ::_thesis: ( C c= B & B c= D )
thus  C c= B by A33, XBOOLE_1:2; ::_thesis: B c= D
thus  B c= D by A42; ::_thesis: verum
end;
suppose C <> {} ; ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )
then consider x being Element of (TOP-REAL 2) such that
A43: C = {x} by A32, Th1;
consider y being Element of D such that
A44: x <> y by Th2;
reconsider y9 = y as Element of (TOP-REAL 2) ;
reconsider Y = {y9} as non empty compact 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 ; ::_thesis: contradiction
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  contradiction ; ::_thesis: verum
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  not Cy is trivial by A45, A44, A49, ZFMISC_1:def_10;
then consider p1, p2 being Point of (TOP-REAL 2), B being 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 ; ::_thesis: ex p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )
take  p2 ; ::_thesis: ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )
take  B ; ::_thesis: ( B is_an_arc_of p1,p2 & C c= B & B c= D )
thus  B is_an_arc_of p1,p2 by A50; ::_thesis: ( C c= B & B c= D )
thus  C c= B by A49, A51, XBOOLE_1:1; ::_thesis: B c= D
thus  B c= D by A52; ::_thesis: verum
end;
end;
end;
suppose not C is trivial ; ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )
hence  ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D ) by A1, A31, A3; ::_thesis: verum
end;
end;
end;