:: JORDAN16 semantic presentation

begin


theorem :: JORDAN16:1
for C being Simple_closed_curve holds Lower_Arc C <> Upper_Arc C
proof
let C be Simple_closed_curve; ::_thesis: Lower_Arc C <> Upper_Arc C
assume  Lower_Arc C = Upper_Arc C ; ::_thesis: contradiction
then A1: Lower_Arc C = (C \ (Lower_Arc C)) \/ {(W-min C),(E-max C)} by JORDAN6:51;
 Lower_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
then A2: ex p3 being Point of (TOP-REAL 2) st
( p3 in Lower_Arc C & p3 <> W-min C & p3 <> E-max C ) by JORDAN6:42;
 Lower_Arc C misses C \ (Lower_Arc C) by XBOOLE_1:79;
then  Lower_Arc C c= {(W-min C),(E-max C)} by A1, XBOOLE_1:73;
hence  contradiction by A2, TARSKI:def_2; ::_thesis: verum
end;

theorem Th2: :: JORDAN16:2
for A being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (A,p1,p2,q1,q2) c= A
proof
let A be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (A,p1,p2,q1,q2) c= A
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: Segment (A,p1,p2,q1,q2) c= A
 Segment (A,p1,p2,q1,q2) = (R_Segment (A,p1,p2,q1)) /\ (L_Segment (A,p1,p2,q2)) by JORDAN6:def_5;
then  ( R_Segment (A,p1,p2,q1) c= A & Segment (A,p1,p2,q1,q2) c= R_Segment (A,p1,p2,q1) ) by JORDAN6:20, XBOOLE_1:17;
hence  Segment (A,p1,p2,q1,q2) c= A by XBOOLE_1:1; ::_thesis: verum
end;

theorem Th3: :: JORDAN16:3
for A being Subset of (TOP-REAL 2)
for q, p1, p2 being Point of (TOP-REAL 2) st q in A holds
q in L_Segment (A,p1,p2,q)
proof
let A be Subset of (TOP-REAL 2); ::_thesis: for q, p1, p2 being Point of (TOP-REAL 2) st q in A holds
q in L_Segment (A,p1,p2,q)
let q, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( q in A implies q in L_Segment (A,p1,p2,q) )
assume  q in A ; ::_thesis: q in L_Segment (A,p1,p2,q)
then A1: LE q,q,A,p1,p2 by JORDAN5C:9;
 L_Segment (A,p1,p2,q) =  {  q1 where q1 is Point of (TOP-REAL 2) : LE q1,q,A,p1,p2  }  by JORDAN6:def_3;
hence  q in L_Segment (A,p1,p2,q) by A1; ::_thesis: verum
end;

theorem Th4: :: JORDAN16:4
for A being Subset of (TOP-REAL 2)
for q, p1, p2 being Point of (TOP-REAL 2) st q in A holds
q in R_Segment (A,p1,p2,q)
proof
let A be Subset of (TOP-REAL 2); ::_thesis: for q, p1, p2 being Point of (TOP-REAL 2) st q in A holds
q in R_Segment (A,p1,p2,q)
let q, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( q in A implies q in R_Segment (A,p1,p2,q) )
assume  q in A ; ::_thesis: q in R_Segment (A,p1,p2,q)
then A1: LE q,q,A,p1,p2 by JORDAN5C:9;
 R_Segment (A,p1,p2,q) =  {  q1 where q1 is Point of (TOP-REAL 2) : LE q,q1,A,p1,p2  }  by JORDAN6:def_4;
hence  q in R_Segment (A,p1,p2,q) by A1; ::_thesis: verum
end;

theorem Th5: :: JORDAN16:5
for A being Subset of (TOP-REAL 2)
for q1, q2, p1, p2 being Point of (TOP-REAL 2) st LE q1,q2,A,p1,p2 holds
( q1 in Segment (A,p1,p2,q1,q2) & q2 in Segment (A,p1,p2,q1,q2) )
proof
let A be Subset of (TOP-REAL 2); ::_thesis: for q1, q2, p1, p2 being Point of (TOP-REAL 2) st LE q1,q2,A,p1,p2 holds
( q1 in Segment (A,p1,p2,q1,q2) & q2 in Segment (A,p1,p2,q1,q2) )
let q1, q2, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( LE q1,q2,A,p1,p2 implies ( q1 in Segment (A,p1,p2,q1,q2) & q2 in Segment (A,p1,p2,q1,q2) ) )
A1: Segment (A,p1,p2,q1,q2) = (R_Segment (A,p1,p2,q1)) /\ (L_Segment (A,p1,p2,q2)) by JORDAN6:def_5;
assume A2: LE q1,q2,A,p1,p2 ; ::_thesis: ( q1 in Segment (A,p1,p2,q1,q2) & q2 in Segment (A,p1,p2,q1,q2) )
 L_Segment (A,p1,p2,q2) =  {  q where q is Point of (TOP-REAL 2) : LE q,q2,A,p1,p2  }  by JORDAN6:def_3;
then A3: q1 in L_Segment (A,p1,p2,q2) by A2;
 q1 in A by A2, JORDAN5C:def_3;
then  q1 in R_Segment (A,p1,p2,q1) by Th4;
hence  q1 in Segment (A,p1,p2,q1,q2) by A1, A3, XBOOLE_0:def_4; ::_thesis: q2 in Segment (A,p1,p2,q1,q2)
 R_Segment (A,p1,p2,q1) =  {  q where q is Point of (TOP-REAL 2) : LE q1,q,A,p1,p2  }  by JORDAN6:def_4;
then A4: q2 in R_Segment (A,p1,p2,q1) by A2;
 q2 in A by A2, JORDAN5C:def_3;
then  q2 in L_Segment (A,p1,p2,q2) by Th3;
hence  q2 in Segment (A,p1,p2,q1,q2) by A1, A4, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: JORDAN16:6
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) holds Segment (p,q,C) c= C
proof
let C be Simple_closed_curve; ::_thesis: for p, q being Point of (TOP-REAL 2) holds Segment (p,q,C) c= C
let p, q be Point of (TOP-REAL 2); ::_thesis: Segment (p,q,C) c= C
set S = Segment (p,q,C);
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Segment (p,q,C) or e in C )
assume A1: e in Segment (p,q,C) ; ::_thesis: e in C
 (Upper_Arc C) \/ (Lower_Arc C) = C by JORDAN6:50;
then A2: ( Upper_Arc C c= C & Lower_Arc C c= C ) by XBOOLE_1:7;
percases ( q = W-min C or q <> W-min C ) ;
suppose q = W-min C ; ::_thesis: e in C
then  Segment (p,q,C) =  {  p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,C or ( p in C & p1 = W-min C ) )  }  by JORDAN7:def_1;
then consider p1 being Point of (TOP-REAL 2) such that
A3: ( e = p1 & ( LE p,p1,C or ( p in C & p1 = W-min C ) ) ) by A1;
now__::_thesis:_(_LE_p,p1,C_implies_p1_in_C_)
assume  LE p,p1,C ; ::_thesis: p1 in C
then  ( p1 in Upper_Arc C or p1 in Lower_Arc C ) by JORDAN6:def_10;
hence  p1 in C by A2; ::_thesis: verum
end;
hence  e in C by A3, SPRECT_1:13; ::_thesis: verum
end;
suppose q <> W-min C ; ::_thesis: e in C
then  Segment (p,q,C) =  {  p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,C & LE p1,q,C )  }  by JORDAN7:def_1;
then consider p1 being Point of (TOP-REAL 2) such that
A4: e = p1 and
A5: LE p,p1,C and
 LE p1,q,C by A1;
 ( p1 in Upper_Arc C or p1 in Lower_Arc C ) by A5, JORDAN6:def_10;
hence  e in C by A2, A4; ::_thesis: verum
end;
end;
end;

theorem :: JORDAN16:7
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st p in C & q in C & not LE p,q,C holds
LE q,p,C
proof
let C be Simple_closed_curve; ::_thesis: for p, q being Point of (TOP-REAL 2) st p in C & q in C & not LE p,q,C holds
LE q,p,C
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in C & q in C & not LE p,q,C implies LE q,p,C )
assume that
A1: p in C and
A2: q in C ; ::_thesis: ( LE p,q,C or LE q,p,C )
A3: C = (Lower_Arc C) \/ (Upper_Arc C) by JORDAN6:50;
percases ( p = q or ( p in Lower_Arc C & p <> W-min C & q in Lower_Arc C & q <> W-min C & p <> q ) or ( p in Lower_Arc C & p <> W-min C & q in Upper_Arc C ) or ( p in Upper_Arc C & q in Lower_Arc C & q <> W-min C ) or ( p in Upper_Arc C & q in Upper_Arc C & p <> q ) ) by A1, A2, A3, JORDAN7:1, XBOOLE_0:def_3;
suppose p = q ; ::_thesis: ( LE p,q,C or LE q,p,C )
hence  ( LE p,q,C or LE q,p,C ) by A1, JORDAN6:56; ::_thesis: verum
end;
supposethat A4: ( p in Lower_Arc C & p <> W-min C & q in Lower_Arc C & q <> W-min C ) and
A5: p <> q ; ::_thesis: ( LE p,q,C or LE q,p,C )
 Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
then  ( LE p,q, Lower_Arc C, E-max C, W-min C or LE q,p, Lower_Arc C, E-max C, W-min C ) by A4, A5, JORDAN5C:14;
hence  ( LE p,q,C or LE q,p,C ) by A4, JORDAN6:def_10; ::_thesis: verum
end;
suppose ( p in Lower_Arc C & p <> W-min C & q in Upper_Arc C ) ; ::_thesis: ( LE p,q,C or LE q,p,C )
hence  ( LE p,q,C or LE q,p,C ) by JORDAN6:def_10; ::_thesis: verum
end;
suppose ( p in Upper_Arc C & q in Lower_Arc C & q <> W-min C ) ; ::_thesis: ( LE p,q,C or LE q,p,C )
hence  ( LE p,q,C or LE q,p,C ) by JORDAN6:def_10; ::_thesis: verum
end;
supposethat A6: ( p in Upper_Arc C & q in Upper_Arc C ) and
A7: p <> q ; ::_thesis: ( LE p,q,C or LE q,p,C )
 Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
then  ( LE p,q, Upper_Arc C, W-min C, E-max C or LE q,p, Upper_Arc C, W-min C, E-max C ) by A6, A7, JORDAN5C:14;
hence  ( LE p,q,C or LE q,p,C ) by A6, JORDAN6:def_10; ::_thesis: verum
end;
end;
end;

theorem Th8: :: JORDAN16:8
for X, Y being non empty TopSpace
for Y0 being non empty SubSpace of Y
for f being Function of X,Y
for g being Function of X,Y0 st f = g & f is continuous holds
g is continuous
proof
let X, Y be non empty TopSpace; ::_thesis: for Y0 being non empty SubSpace of Y
for f being Function of X,Y
for g being Function of X,Y0 st f = g & f is continuous holds
g is continuous
let Y0 be non empty SubSpace of Y; ::_thesis: for f being Function of X,Y
for g being Function of X,Y0 st f = g & f is continuous holds
g is continuous
let f be Function of X,Y; ::_thesis: for g being Function of X,Y0 st f = g & f is continuous holds
g is continuous
let g be Function of X,Y0; ::_thesis: ( f = g & f is continuous implies g is continuous )
assume that
A1: f = g and
A2: f is continuous ; ::_thesis: g is continuous
let W be Point of X; :: according to BORSUK_1:def_1 ::_thesis: for b1 being a_neighborhood of g . W ex b2 being a_neighborhood of W st g .: b2 c= b1
let G be a_neighborhood of g . W; ::_thesis: ex b1 being a_neighborhood of W st g .: b1 c= G
consider V being Subset of Y0 such that
A3: V is open and
A4: V c= G and
A5: g . W in V by CONNSP_2:6;
 ( g . W in [#] Y0 & [#] Y0 c= [#] Y ) by PRE_TOPC:def_4;
then reconsider p = g . W as Point of Y ;
consider C being Subset of Y such that
A6: C is open and
A7: C /\ ([#] Y0) = V by A3, TOPS_2:24;
 p in C by A5, A7, XBOOLE_0:def_4;
then  C is a_neighborhood of p by A6, CONNSP_2:3;
then consider H being a_neighborhood of W such that
A8: f .: H c= C by A1, A2, BORSUK_1:def_1;
take  H ; ::_thesis: g .: H c= G
 g .: H c= V by A1, A7, A8, XBOOLE_1:19;
hence  g .: H c= G by A4, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th9: :: JORDAN16:9
for S, T being non empty TopSpace
for S0 being non empty SubSpace of S
for T0 being non empty SubSpace of T
for f being Function of S,T st f is being_homeomorphism holds
for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is being_homeomorphism
proof
let S, T be non empty TopSpace; ::_thesis: for S0 being non empty SubSpace of S
for T0 being non empty SubSpace of T
for f being Function of S,T st f is being_homeomorphism holds
for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is being_homeomorphism
let S0 be non empty SubSpace of S; ::_thesis: for T0 being non empty SubSpace of T
for f being Function of S,T st f is being_homeomorphism holds
for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is being_homeomorphism
let T0 be non empty SubSpace of T; ::_thesis: for f being Function of S,T st f is being_homeomorphism holds
for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is being_homeomorphism
let f be Function of S,T; ::_thesis: ( f is being_homeomorphism implies for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is being_homeomorphism )
assume A1: f is being_homeomorphism ; ::_thesis: for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is being_homeomorphism
A2: rng f = [#] T by A1, TOPS_2:def_5;
A3: f " is continuous by A1, TOPS_2:def_5;
let g be Function of S0,T0; ::_thesis: ( g = f | S0 & g is onto implies g is being_homeomorphism )
assume that
A4: g = f | S0 and
A5: g is onto ; ::_thesis: g is being_homeomorphism
A6: g = f | the carrier of S0 by A4, TMAP_1:def_4;
then A7: f .: the carrier of S0 = rng g by RELAT_1:115
.= the carrier of T0 by A5, FUNCT_2:def_3 ;
thus  dom g = [#] S0 by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng g = [#] T0 & g is one-to-one & g is continuous & g " is continuous )
thus  rng g = [#] T0 by A5, FUNCT_2:def_3; ::_thesis: ( g is one-to-one & g is continuous & g " is continuous )
A8: f is one-to-one by A1, TOPS_2:def_5;
hence A9: g is one-to-one by A6, FUNCT_1:52; ::_thesis: ( g is continuous & g " is continuous )
A10: f is onto by A2, FUNCT_2:def_3;
 f is continuous by A1, TOPS_2:def_5;
then  g is continuous Function of S0,T by A4;
hence  g is continuous by Th8; ::_thesis: g " is continuous
g " = (f | the carrier of S0) " by A5, A6, A9, TOPS_2:def_4
.= (f ") | (f .: the carrier of S0) by A8, RFUNCT_2:17
.= (f ") | the carrier of T0 by A10, A8, A7, TOPS_2:def_4
.= (f ") | T0 by TMAP_1:def_4 ;
then  g " is continuous Function of T0,S by A3;
hence  g " is continuous by Th8; ::_thesis: verum
end;

theorem Th10: :: JORDAN16:10
for P1, P2, P3 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P3 is_an_arc_of p1,p2 & P2 /\ P3 = {p1,p2} & P1 c= P2 \/ P3 & not P1 = P2 holds
P1 = P3
proof
let P1, P2, P3 be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P3 is_an_arc_of p1,p2 & P2 /\ P3 = {p1,p2} & P1 c= P2 \/ P3 & not P1 = P2 holds
P1 = P3
set P = P2 \/ P3;
A1: the carrier of ((TOP-REAL 2) | (P2 \/ P3)) = [#] ((TOP-REAL 2) | (P2 \/ P3))
.= P2 \/ P3 by PRE_TOPC:def_5 ;
then reconsider U2 = P2 as Subset of ((TOP-REAL 2) | (P2 \/ P3)) by XBOOLE_1:7;
reconsider U3 = P3 as Subset of ((TOP-REAL 2) | (P2 \/ P3)) by A1, XBOOLE_1:7;
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P3 is_an_arc_of p1,p2 & P2 /\ P3 = {p1,p2} & P1 c= P2 \/ P3 & not P1 = P2 implies P1 = P3 )
assume that
A2: P1 is_an_arc_of p1,p2 and
A3: P2 is_an_arc_of p1,p2 and
A4: P3 is_an_arc_of p1,p2 ; ::_thesis: ( not P2 /\ P3 = {p1,p2} or not P1 c= P2 \/ P3 or P1 = P2 or P1 = P3 )
consider f being Function of I[01],((TOP-REAL 2) | P1) such that
A5: f is being_homeomorphism and
A6: ( f . 0 = p1 & f . 1 = p2 ) by A2, TOPREAL1:def_1;
A7: f is one-to-one by A5, TOPS_2:def_5;
 U2 = P2 /\ (P2 \/ P3) by XBOOLE_1:7, XBOOLE_1:28;
then A8: U2 is closed by A3, JORDAN6:2, JORDAN6:11;
A9: rng f = [#] ((TOP-REAL 2) | P1) by A5, TOPS_2:def_5
.= P1 by PRE_TOPC:def_5 ;
 p1 in P2 by A3, TOPREAL1:1;
then reconsider Q = P2 \/ P3 as non empty Subset of (Euclid 2) by TOPREAL3:8;
assume that
A10: P2 /\ P3 = {p1,p2} and
A11: P1 c= P2 \/ P3 ; ::_thesis: ( P1 = P2 or P1 = P3 )
A12: ( p2 in P2 /\ P3 & p1 in P2 /\ P3 ) by A10, TARSKI:def_2;
 U3 = P3 /\ (P2 \/ P3) by XBOOLE_1:7, XBOOLE_1:28;
then A13: U3 is closed by A4, JORDAN6:2, JORDAN6:11;
A14: f is continuous by A5, TOPS_2:def_5;
A15: dom f = [#] I[01] by A5, TOPS_2:def_5;
percases ( for r being Real st 0 < r & r < 1 holds
f . r in P3 or ex r being Real st
( 0 < r & r < 1 & not f . r in P3 ) ) ;
supposeA16: for r being Real st 0 < r & r < 1 holds
f . r in P3 ; ::_thesis: ( P1 = P2 or P1 = P3 )
 P1 c= P3
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in P1 or y in P3 )
assume  y in P1 ; ::_thesis: y in P3
then consider x being set  such that
A17: x in dom f and
A18: y = f . x by A9, FUNCT_1:def_3;
reconsider r = x as Real by A15, A17, BORSUK_1:40;
 r <= 1 by A17, BORSUK_1:40, XXREAL_1:1;
then  ( r = 0 or r = 1 or ( 0 < r & r < 1 ) ) by A17, BORSUK_1:40, XXREAL_0:1, XXREAL_1:1;
hence  y in P3 by A12, A6, A16, A18, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  ( P1 = P2 or P1 = P3 ) by A2, A4, JORDAN6:46; ::_thesis: verum
end;
supposeA19: ex r being Real st
( 0 < r & r < 1 & not f . r in P3 ) ; ::_thesis: ( P1 = P2 or P1 = P3 )
now__::_thesis:_(_(_(_for_r_being_Real_st_0_<_r_&_r_<_1_holds_
f_._r_in_P2_)_&_(_P1_=_P2_or_P1_=_P3_)_)_or_(_ex_r_being_Real_st_
(_0_<_r_&_r_<_1_&_not_f_._r_in_P2_)_&_contradiction_)_)
percases ( for r being Real st 0 < r & r < 1 holds
f . r in P2 or ex r being Real st
( 0 < r & r < 1 & not f . r in P2 ) ) ;
caseA20: for r being Real st 0 < r & r < 1 holds
f . r in P2 ; ::_thesis: ( P1 = P2 or P1 = P3 )
 P1 c= P2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in P1 or y in P2 )
assume  y in P1 ; ::_thesis: y in P2
then consider x being set  such that
A21: x in dom f and
A22: y = f . x by A9, FUNCT_1:def_3;
reconsider r = x as Real by A15, A21, BORSUK_1:40;
 r <= 1 by A21, BORSUK_1:40, XXREAL_1:1;
then  ( ( 0 < r & r < 1 ) or r = 0 or r = 1 ) by A21, BORSUK_1:40, XXREAL_0:1, XXREAL_1:1;
hence  y in P2 by A12, A6, A20, A22, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  ( P1 = P2 or P1 = P3 ) by A2, A3, JORDAN6:46; ::_thesis: verum
end;
case ex r being Real st
( 0 < r & r < 1 & not f . r in P2 ) ; ::_thesis: contradiction
then consider r2 being Real such that
A23: 0 < r2 and
A24: r2 < 1 and
A25: not f . r2 in P2 ;
 r2 in [.0,1.] by A23, A24, XXREAL_1:1;
then  f . r2 in rng f by A15, BORSUK_1:40, FUNCT_1:def_3;
then A26: f . r2 in P3 by A11, A9, A25, XBOOLE_0:def_3;
consider r1 being Real such that
A27: 0 < r1 and
A28: r1 < 1 and
A29: not f . r1 in P3 by A19;
 r1 in [.0,1.] by A27, A28, XXREAL_1:1;
then A30: f . r1 in rng f by A15, BORSUK_1:40, FUNCT_1:def_3;
then A31: f . r1 in P2 by A11, A9, A29, XBOOLE_0:def_3;
now__::_thesis:_contradiction
percases ( r1 <= r2 or r1 > r2 ) ;
supposeA32: r1 <= r2 ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( r1 = r2 or r1 < r2 ) by A32, XXREAL_0:1;
suppose r1 = r2 ; ::_thesis: contradiction
hence  contradiction by A11, A9, A25, A29, A30, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA33: r1 < r2 ; ::_thesis: contradiction
A34: the carrier of ((TOP-REAL 2) | P1) = [#] ((TOP-REAL 2) | P1)
.= P1 by PRE_TOPC:def_5 ;
the carrier of ((TOP-REAL 2) | (P2 \/ P3)) = [#] ((TOP-REAL 2) | (P2 \/ P3))
.= P2 \/ P3 by PRE_TOPC:def_5 ;
then  rng f c= the carrier of ((TOP-REAL 2) | (P2 \/ P3)) by A11, A34, XBOOLE_1:1;
then reconsider g = f as Function of I[01],((TOP-REAL 2) | (P2 \/ P3)) by A15, FUNCT_2:2;
 P2 \/ P3 = P1 \/ (P2 \/ P3) by A11, XBOOLE_1:12;
then A35: (TOP-REAL 2) | P1 is SubSpace of (TOP-REAL 2) | (P2 \/ P3) by TOPMETR:4;
 ( U2 \/ U3 = the carrier of ((Euclid 2) | Q) & (TOP-REAL 2) | (P2 \/ P3) = TopSpaceMetr ((Euclid 2) | Q) ) by EUCLID:63, TOPMETR:def_2;
then consider r0 being Real such that
A36: r1 <= r0 and
A37: r0 <= r2 and
A38: g . r0 in U2 /\ U3 by A14, A8, A13, A24, A27, A26, A31, A33, A35, PRE_TOPC:26, TOPMETR3:13;
 r0 < 1 by A24, A37, XXREAL_0:2;
then A39: r0 in dom f by A15, A27, A36, BORSUK_1:40, XXREAL_1:1;
A40: ( 0 in dom f & 1 in dom f ) by A15, BORSUK_1:40, XXREAL_1:1;
 ( g . r0 = p1 or g . r0 = p2 ) by A10, A38, TARSKI:def_2;
hence  contradiction by A6, A7, A24, A27, A36, A37, A39, A40, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
supposeA41: r1 > r2 ; ::_thesis: contradiction
A42: the carrier of ((TOP-REAL 2) | P1) = [#] ((TOP-REAL 2) | P1)
.= P1 by PRE_TOPC:def_5 ;
the carrier of ((TOP-REAL 2) | (P2 \/ P3)) = [#] ((TOP-REAL 2) | (P2 \/ P3))
.= P2 \/ P3 by PRE_TOPC:def_5 ;
then  rng f c= the carrier of ((TOP-REAL 2) | (P2 \/ P3)) by A11, A42, XBOOLE_1:1;
then reconsider g = f as Function of I[01],((TOP-REAL 2) | (P2 \/ P3)) by A15, FUNCT_2:2;
 P2 \/ P3 = P1 \/ (P2 \/ P3) by A11, XBOOLE_1:12;
then A43: (TOP-REAL 2) | P1 is SubSpace of (TOP-REAL 2) | (P2 \/ P3) by TOPMETR:4;
 ( U2 \/ U3 = the carrier of ((Euclid 2) | Q) & (TOP-REAL 2) | (P2 \/ P3) = TopSpaceMetr ((Euclid 2) | Q) ) by EUCLID:63, TOPMETR:def_2;
then consider r0 being Real such that
A44: r2 <= r0 and
A45: r0 <= r1 and
A46: g . r0 in U2 /\ U3 by A14, A8, A13, A23, A28, A26, A31, A41, A43, PRE_TOPC:26, TOPMETR3:13;
 r0 < 1 by A28, A45, XXREAL_0:2;
then A47: r0 in dom f by A15, A23, A44, BORSUK_1:40, XXREAL_1:1;
A48: ( 0 in dom f & 1 in dom f ) by A15, BORSUK_1:40, XXREAL_1:1;
 ( g . r0 = p1 or g . r0 = p2 ) by A10, A46, TARSKI:def_2;
hence  contradiction by A6, A7, A23, A28, A44, A45, A47, A48, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
hence  ( P1 = P2 or P1 = P3 ) ; ::_thesis: verum
end;
end;
end;

theorem Th11: :: JORDAN16:11
for C being Simple_closed_curve
for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 <> A2 holds
( A1 \/ A2 = C & A1 /\ A2 = {p1,p2} )
proof
let C be Simple_closed_curve; ::_thesis: for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 <> A2 holds
( A1 \/ A2 = C & A1 /\ A2 = {p1,p2} )
let A1, A2 be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 <> A2 holds
( A1 \/ A2 = C & A1 /\ A2 = {p1,p2} )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 <> A2 implies ( A1 \/ A2 = C & A1 /\ A2 = {p1,p2} ) )
assume that
A1: A1 is_an_arc_of p1,p2 and
A2: A2 is_an_arc_of p1,p2 and
A3: A1 c= C and
A4: ( A2 c= C & A1 <> A2 ) ; ::_thesis: ( A1 \/ A2 = C & A1 /\ A2 = {p1,p2} )
A5: p2 in A1 by A1, TOPREAL1:1;
 ( p1 <> p2 & p1 in A1 ) by A1, JORDAN6:37, TOPREAL1:1;
then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A6: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & C = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) by A3, A5, TOPREAL2:5;
reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) ;
 ( A1 = P1 or A1 = P2 ) by A1, A3, A6, Th10;
hence  ( A1 \/ A2 = C & A1 /\ A2 = {p1,p2} ) by A2, A4, A6, Th10; ::_thesis: verum
end;

theorem Th12: :: JORDAN16:12
for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A1 /\ A2 = {q1,q2} holds
A1 <> A2
proof
let A1, A2 be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A1 /\ A2 = {q1,q2} holds
A1 <> A2
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( A1 is_an_arc_of p1,p2 & A1 /\ A2 = {q1,q2} implies A1 <> A2 )
assume that
A1: A1 is_an_arc_of p1,p2 and
A2: ( A1 /\ A2 = {q1,q2} & A1 = A2 ) ; ::_thesis: contradiction
 p1 in A1 by A1, TOPREAL1:1;
then A3: ( p1 = q1 or p1 = q2 ) by A2, TARSKI:def_2;
 p2 in A1 by A1, TOPREAL1:1;
then A4: ( p2 = q1 or p2 = q2 ) by A2, TARSKI:def_2;
 ex p3 being Point of (TOP-REAL 2) st
( p3 in A1 & p3 <> p1 & p3 <> p2 ) by A1, JORDAN6:42;
hence  contradiction by A1, A2, A3, A4, JORDAN6:37, TARSKI:def_2; ::_thesis: verum
end;

theorem :: JORDAN16:13
for C being Simple_closed_curve
for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 /\ A2 = {p1,p2} holds
A1 \/ A2 = C
proof
let C be Simple_closed_curve; ::_thesis: for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 /\ A2 = {p1,p2} holds
A1 \/ A2 = C
let A1, A2 be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 /\ A2 = {p1,p2} holds
A1 \/ A2 = C
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 /\ A2 = {p1,p2} implies A1 \/ A2 = C )
assume that
A1: A1 is_an_arc_of p1,p2 and
A2: A2 is_an_arc_of p1,p2 and
A3: ( A1 c= C & A2 c= C ) and
A4: A1 /\ A2 = {p1,p2} ; ::_thesis: A1 \/ A2 = C
 A1 <> A2 by A2, A4, Th12;
hence  A1 \/ A2 = C by A1, A2, A3, Th11; ::_thesis: verum
end;

theorem :: JORDAN16:14
for C being Simple_closed_curve
for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 holds
for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds
A = A2
proof
let C be Simple_closed_curve; ::_thesis: for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 holds
for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds
A = A2
let A1, A2 be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 holds
for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds
A = A2
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 implies for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds
A = A2 )
assume that
A1: ( A1 c= C & A2 c= C & A1 <> A2 ) and
A2: ( A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 ) ; ::_thesis: for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds
A = A2
A3: ( A1 \/ A2 = C & A1 /\ A2 = {p1,p2} ) by A1, A2, Th11;
let A be Subset of (TOP-REAL 2); ::_thesis: ( A is_an_arc_of p1,p2 & A c= C & not A = A1 implies A = A2 )
assume  ( A is_an_arc_of p1,p2 & A c= C ) ; ::_thesis: ( A = A1 or A = A2 )
hence  ( A = A1 or A = A2 ) by A2, A3, Th10; ::_thesis: verum
end;

theorem Th15: :: JORDAN16:15
for C being Simple_closed_curve
for A being non empty Subset of (TOP-REAL 2) st A is_an_arc_of W-min C, E-max C & A c= C & not A = Lower_Arc C holds
A = Upper_Arc C
proof
let C be Simple_closed_curve; ::_thesis: for A being non empty Subset of (TOP-REAL 2) st A is_an_arc_of W-min C, E-max C & A c= C & not A = Lower_Arc C holds
A = Upper_Arc C
let A be non empty Subset of (TOP-REAL 2); ::_thesis: ( A is_an_arc_of W-min C, E-max C & A c= C & not A = Lower_Arc C implies A = Upper_Arc C )
assume that
A1: A is_an_arc_of W-min C, E-max C and
A2: A c= C ; ::_thesis: ( A = Lower_Arc C or A = Upper_Arc C )
 A is compact by A1, JORDAN5A:1;
hence  ( A = Lower_Arc C or A = Upper_Arc C ) by A1, A2, TOPMETR3:15; ::_thesis: verum
end;

theorem Th16: :: JORDAN16:16
for A being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 holds
ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
proof
let A be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 holds
ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 implies ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 ) )
given f being Function of I[01],((TOP-REAL 2) | A) such that A1: f is being_homeomorphism and
A2: ( f . 0 = p1 & f . 1 = p2 ) ; :: according to TOPREAL1:def_1 ::_thesis: ( not LE q1,q2,A,p1,p2 or ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 ) )
A3: rng f = [#] ((TOP-REAL 2) | A) by A1, TOPS_2:def_5
.= A by PRE_TOPC:def_5 ;
assume A4: LE q1,q2,A,p1,p2 ; ::_thesis: ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
then  q1 in A by JORDAN5C:def_3;
then consider u being set  such that
A5: u in dom f and
A6: q1 = f . u by A3, FUNCT_1:def_3;
take  f ; ::_thesis: ex s1, s2 being Real st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s1 = q1 & f . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
A7: dom f = [#] I[01] by A1, TOPS_2:def_5
.= [.0,1.] by BORSUK_1:40 ;
then reconsider s1 = u as Element of REAL by A5;
A8: s1 <= 1 by A7, A5, XXREAL_1:1;
 q2 in A by A4, JORDAN5C:def_3;
then consider u being set  such that
A9: u in dom f and
A10: q2 = f . u by A3, FUNCT_1:def_3;
reconsider s2 = u as Element of REAL by A7, A9;
take  s1 ; ::_thesis: ex s2 being Real st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s1 = q1 & f . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
take  s2 ; ::_thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s1 = q1 & f . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
thus  ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A1, A2; ::_thesis: ( f . s1 = q1 & f . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
thus  ( q1 = f . s1 & q2 = f . s2 ) by A6, A10; ::_thesis: ( 0 <= s1 & s1 <= s2 & s2 <= 1 )
thus  0 <= s1 by A7, A5, XXREAL_1:1; ::_thesis: ( s1 <= s2 & s2 <= 1 )
 ( 0 <= s2 & s2 <= 1 ) by A7, A9, XXREAL_1:1;
hence  s1 <= s2 by A1, A2, A4, A6, A10, A8, JORDAN5C:def_3; ::_thesis: s2 <= 1
thus  s2 <= 1 by A7, A9, XXREAL_1:1; ::_thesis: verum
end;

theorem Th17: :: JORDAN16:17
for A being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 holds
ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 < s2 & s2 <= 1 )
proof
let A be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 holds
ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 < s2 & s2 <= 1 )
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 implies ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 < s2 & s2 <= 1 ) )
assume that
A1: ( A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 ) and
A2: q1 <> q2 ; ::_thesis: ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 < s2 & s2 <= 1 )
consider g being Function of I[01],((TOP-REAL 2) | A), s1, s2 being Real such that
A3: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 ) and
A4: ( g . s1 = q1 & g . s2 = q2 ) and
A5: 0 <= s1 and
A6: s1 <= s2 and
A7: s2 <= 1 by A1, Th16;
take  g ; ::_thesis: ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 < s2 & s2 <= 1 )
take  s1 ; ::_thesis: ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 < s2 & s2 <= 1 )
take  s2 ; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 < s2 & s2 <= 1 )
thus  ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 ) by A3, A4, A5; ::_thesis: ( s1 < s2 & s2 <= 1 )
thus  s1 < s2 by A2, A4, A6, XXREAL_0:1; ::_thesis: s2 <= 1
thus  s2 <= 1 by A7; ::_thesis: verum
end;

theorem :: JORDAN16:18
for A being Subset of (TOP-REAL 2)
for q1, q2, p1, p2 being Point of (TOP-REAL 2) st LE q1,q2,A,p1,p2 holds
not Segment (A,p1,p2,q1,q2) is empty
proof
let A be Subset of (TOP-REAL 2); ::_thesis: for q1, q2, p1, p2 being Point of (TOP-REAL 2) st LE q1,q2,A,p1,p2 holds
not Segment (A,p1,p2,q1,q2) is empty
let q1, q2, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( LE q1,q2,A,p1,p2 implies not Segment (A,p1,p2,q1,q2) is empty )
A1: Segment (A,p1,p2,q1,q2) =  {  q where q is Point of (TOP-REAL 2) : ( LE q1,q,A,p1,p2 & LE q,q2,A,p1,p2 )  }  by JORDAN6:26;
assume A2: LE q1,q2,A,p1,p2 ; ::_thesis: not Segment (A,p1,p2,q1,q2) is empty
then  q2 in A by JORDAN5C:def_3;
then  LE q2,q2,A,p1,p2 by JORDAN5C:9;
then  q2 in Segment (A,p1,p2,q1,q2) by A2, A1;
hence  not Segment (A,p1,p2,q1,q2) is empty ; ::_thesis: verum
end;

theorem :: JORDAN16:19
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p in C holds
( p in Segment (p,(W-min C),C) & W-min C in Segment (p,(W-min C),C) )
proof
let C be Simple_closed_curve; ::_thesis: for p being Point of (TOP-REAL 2) st p in C holds
( p in Segment (p,(W-min C),C) & W-min C in Segment (p,(W-min C),C) )
let p be Point of (TOP-REAL 2); ::_thesis: ( p in C implies ( p in Segment (p,(W-min C),C) & W-min C in Segment (p,(W-min C),C) ) )
A1: Segment (p,(W-min C),C) =  {  p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,C or ( p in C & p1 = W-min C ) )  }  by JORDAN7:def_1;
assume A2: p in C ; ::_thesis: ( p in Segment (p,(W-min C),C) & W-min C in Segment (p,(W-min C),C) )
then  LE p,p,C by JORDAN6:56;
hence  p in Segment (p,(W-min C),C) by A1; ::_thesis: W-min C in Segment (p,(W-min C),C)
thus  W-min C in Segment (p,(W-min C),C) by A2, A1; ::_thesis: verum
end;

theorem Th20: :: JORDAN16:20
for f being Function of R^1,R^1
for a, b being Real st a <> 0 & f = AffineMap (a,b) holds
f is being_homeomorphism
proof
let f be Function of R^1,R^1; ::_thesis: for a, b being Real st a <> 0 & f = AffineMap (a,b) holds
f is being_homeomorphism
let a, b be Real; ::_thesis: ( a <> 0 & f = AffineMap (a,b) implies f is being_homeomorphism )
assume that
A1: a <> 0 and
A2: f = AffineMap (a,b) ; ::_thesis: f is being_homeomorphism
thus  dom f = [#] R^1 by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng f = [#] R^1 & f is one-to-one & f is continuous & f " is continuous )
thus A3: rng f = [#] R^1 by A1, A2, FCONT_1:55, TOPMETR:17; ::_thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus A4: f is one-to-one by A1, A2, FCONT_1:50; ::_thesis: ( f is continuous & f " is continuous )
 for x being Real holds f . x = (a * x) + b by A2, FCONT_1:def_4;
hence  f is continuous by TOPMETR:21; ::_thesis: f " is continuous
 f is onto by A3, FUNCT_2:def_3;
then f " = f " by A4, TOPS_2:def_4
.= AffineMap ((a "),(- (b / a))) by A1, A2, FCONT_1:56 ;
then  for x being Real holds (f ") . x = ((a ") * x) + (- (b / a)) by FCONT_1:def_4;
hence  f " is continuous by TOPMETR:21; ::_thesis: verum
end;

theorem Th21: :: JORDAN16:21
for A being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 holds
Segment (A,p1,p2,q1,q2) is_an_arc_of q1,q2
proof
let A be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 holds
Segment (A,p1,p2,q1,q2) is_an_arc_of q1,q2
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 implies Segment (A,p1,p2,q1,q2) is_an_arc_of q1,q2 )
assume that
A1: A is_an_arc_of p1,p2 and
A2: ( LE q1,q2,A,p1,p2 & q1 <> q2 ) ; ::_thesis: Segment (A,p1,p2,q1,q2) is_an_arc_of q1,q2
consider g being Function of I[01],((TOP-REAL 2) | A), s1, s2 being Real such that
A3: g is being_homeomorphism and
A4: ( g . 0 = p1 & g . 1 = p2 ) and
A5: g . s1 = q1 and
A6: g . s2 = q2 and
A7: 0 <= s1 and
A8: s1 < s2 and
A9: s2 <= 1 by A1, A2, Th17;
reconsider A9 = A as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;
set S = Segment (A,p1,p2,q1,q2);
A10: Segment (A,p1,p2,q1,q2) =  {  q where q is Point of (TOP-REAL 2) : ( LE q1,q,A,p1,p2 & LE q,q2,A,p1,p2 )  }  by JORDAN6:26;
A11: 0 < s2 - s1 by A8, XREAL_1:50;
set f = (g * (AffineMap ((s2 - s1),s1))) | [.0,1.];
reconsider g = g as Function of I[01],((TOP-REAL 2) | A9) ;
reconsider m = AffineMap ((s2 - s1),s1) as Function of R^1,R^1 by TOPMETR:17;
 for x being Real holds m . x = ((s2 - s1) * x) + s1 by FCONT_1:def_4;
then reconsider m = m as continuous Function of R^1,R^1 by TOPMETR:21;
set h = m | I[01];
A12: m | I[01] = m | [.0,1.] by BORSUK_1:40, TMAP_1:def_4;
then A13: rng (m | I[01]) = m .: [.0,1.] by RELAT_1:115
.= [.s1,((s2 - s1) + s1).] by A8, FCONT_1:57, XREAL_1:50
.= [.s1,s2.] ;
then A14: rng (m | I[01]) c= [.0,1.] by A7, A9, XXREAL_1:34;
A15: dom m = REAL by FUNCT_2:def_1;
then A16: dom (m | I[01]) = [.0,1.] by A12, RELAT_1:62;
then reconsider h = m | I[01] as Function of I[01],I[01] by A14, BORSUK_1:40, RELSET_1:4;
A17: (g * (AffineMap ((s2 - s1),s1))) | [.0,1.] = g * h by A12, RELAT_1:83;
A18: [.0,1.] = dom g by BORSUK_1:40, FUNCT_2:def_1;
 m .: [.0,1.] c= dom g
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in m .: [.0,1.] or e in dom g )
assume  e in m .: [.0,1.] ; ::_thesis: e in dom g
then A19: e in [.s1,((s2 - s1) + s1).] by A8, FCONT_1:57, XREAL_1:50;
 [.s1,s2.] c= [.0,1.] by A7, A9, XXREAL_1:34;
hence  e in dom g by A18, A19; ::_thesis: verum
end;
then A20: [.0,1.] c= dom (g * m) by A15, FUNCT_3:3;
then A21: dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) = [#] I[01] by BORSUK_1:40, RELAT_1:62;
reconsider CIT = Closed-Interval-TSpace (s1,s2) as non empty SubSpace of I[01] by A7, A8, A9, TOPMETR:20, TREAL_1:3;
 [.s1,s2.] c= [.0,1.] by A7, A9, XXREAL_1:34;
then A22: the carrier of CIT c= dom g by A8, A18, TOPMETR:18;
A23: rng h = the carrier of CIT by A8, A13, TOPMETR:18;
A24: dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) = the carrier of I[01] by A20, BORSUK_1:40, RELAT_1:62;
A25: s1 < 1 by A8, A9, XXREAL_0:2;
 for y being set holds
( y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) iff ex x being set st
( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x ) )
proof
let y be set ; ::_thesis: ( y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) iff ex x being set st
( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x ) )
thus  ( y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) implies ex x being set st
( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x ) ) ::_thesis: ( ex x being set st
( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x ) implies y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) )
proof
assume  y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) ; ::_thesis: ex x being set st
( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x )
then  y in Segment (A,p1,p2,q1,q2) by PRE_TOPC:def_5;
then consider q0 being Point of (TOP-REAL 2) such that
A26: y = q0 and
A27: LE q1,q0,A,p1,p2 and
A28: LE q0,q2,A,p1,p2 by A10;
 q0 in A by A27, JORDAN5C:def_3;
then  q0 in [#] ((TOP-REAL 2) | A) by PRE_TOPC:def_5;
then  q0 in rng g by A3, TOPS_2:def_5;
then consider s being set  such that
A29: s in dom g and
A30: q0 = g . s by FUNCT_1:def_3;
reconsider s = s as Element of REAL by A18, A29;
take x = (s - s1) / (s2 - s1); ::_thesis: ( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x )
A31: s <= 1 by A29, BORSUK_1:40, XXREAL_1:1;
then  s <= s2 by A3, A4, A6, A7, A8, A9, A28, A30, JORDAN5C:def_3;
then  s - s1 <= s2 - s1 by XREAL_1:9;
then  x <= (s2 - s1) / (s2 - s1) by A11, XREAL_1:72;
then A32: x <= 1 by A11, XCMPLX_1:60;
 0 <= s by A29, BORSUK_1:40, XXREAL_1:1;
then  s1 + 0 <= s by A3, A4, A5, A25, A27, A30, A31, JORDAN5C:def_3;
then  0 <= s - s1 by XREAL_1:19;
hence A33: x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) by A11, A21, A32, BORSUK_1:40, XXREAL_1:1; ::_thesis: y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x
m . x = ((s2 - s1) * x) + s1 by FCONT_1:def_4
.= (s - s1) + s1 by A11, XCMPLX_1:87
.= s ;
hence y = (g * m) . x by A15, A26, A30, FUNCT_1:13
.= ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x by A33, FUNCT_1:47 ;
::_thesis: verum
end;
given x being set  such that A34: x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) and
A35: y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x ; ::_thesis: y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2)))
reconsider x = x as Element of REAL by A34;
 (AffineMap ((s2 - s1),s1)) . x in REAL ;
then reconsider s = m . x as Element of REAL ;
 h . x = m . x by A12, A16, A21, A34, BORSUK_1:40, FUNCT_1:47;
then A36: s in rng h by A16, A21, A34, BORSUK_1:40, FUNCT_1:def_3;
then A37: s1 <= s by A13, XXREAL_1:1;
 y in rng ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) by A34, A35, FUNCT_1:def_3;
then  y in [#] ((TOP-REAL 2) | A) ;
then  y in A by PRE_TOPC:def_5;
then reconsider q = y as Point of (TOP-REAL 2) ;
A38: s <= s2 by A13, A36, XXREAL_1:1;
then A39: s <= 1 by A9, XXREAL_0:2;
A40: q = (g * m) . x by A34, A35, FUNCT_1:47
.= g . s by A15, FUNCT_1:13 ;
then A41: LE q1,q,A,p1,p2 by A1, A3, A4, A5, A7, A25, A37, A39, JORDAN5C:8;
 LE q,q2,A,p1,p2 by A1, A3, A4, A6, A7, A9, A40, A37, A38, A39, JORDAN5C:8;
then  q in Segment (A,p1,p2,q1,q2) by A10, A41;
hence  y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) by PRE_TOPC:def_5; ::_thesis: verum
end;
then A42: rng ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) = [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) by FUNCT_1:def_3;
then A43: [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) <> {} by A21, RELAT_1:42;
then reconsider f = (g * (AffineMap ((s2 - s1),s1))) | [.0,1.] as Function of I[01],((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) by A24, A42, FUNCT_2:def_1, RELSET_1:4;
reconsider TS = (TOP-REAL 2) | (Segment (A,p1,p2,q1,q2)) as non empty SubSpace of (TOP-REAL 2) | A9 by A43, Th2, TOPMETR:22;
take  f ; :: according to TOPREAL1:def_1 ::_thesis: ( f is being_homeomorphism & f . 0 = q1 & f . 1 = q2 )
A44: (AffineMap ((s2 - s1),s1)) . 0 = s1 by FCONT_1:48;
set o = g | CIT;
A45: dom (g | CIT) = dom (g | the carrier of CIT) by TMAP_1:def_4
.= (dom g) /\ the carrier of CIT by RELAT_1:61
.= the carrier of CIT by A22, XBOOLE_1:28 ;
reconsider h = h as Function of I[01],CIT by A16, A23, RELSET_1:4;
 h is onto by A23, FUNCT_2:def_3;
then A46: h is being_homeomorphism by A11, Th9, Th20;
A47: the carrier of CIT = [.s1,s2.] by A8, TOPMETR:18;
then  g | CIT = g | (rng h) by A13, TMAP_1:def_4;
then A48: f = (g | CIT) * h by A17, FUNCT_4:2;
then A49: rng (g | CIT) = rng f by A13, A45, A47, RELAT_1:28;
then reconsider o = g | CIT as Function of CIT,TS by A45, RELSET_1:4;
 o is onto by A42, A49, FUNCT_2:def_3;
then  o is being_homeomorphism by A3, Th9;
hence  f is being_homeomorphism by A48, A46, TOPS_2:57; ::_thesis: ( f . 0 = q1 & f . 1 = q2 )
A50: dom (AffineMap ((s2 - s1),s1)) = REAL by FUNCT_2:def_1;
 0 in [.0,1.] by XXREAL_1:1;
hence f . 0 = (g * m) . 0 by FUNCT_1:49
.= q1 by A5, A44, A50, FUNCT_1:13 ;
::_thesis: f . 1 = q2
A51: (AffineMap ((s2 - s1),s1)) . 1 = (s2 - s1) + s1 by FCONT_1:49
.= s2 ;
 1 in [.0,1.] by XXREAL_1:1;
hence f . 1 = (g * m) . 1 by FUNCT_1:49
.= q2 by A6, A51, A50, FUNCT_1:13 ;
::_thesis: verum
end;

theorem :: JORDAN16:22
for C being Simple_closed_curve
for p1, p2 being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st P c= C & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P & not Upper_Arc C c= P holds
Lower_Arc C c= P
proof
let C be Simple_closed_curve; ::_thesis: for p1, p2 being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st P c= C & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P & not Upper_Arc C c= P holds
Lower_Arc C c= P
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: for P being Subset of (TOP-REAL 2) st P c= C & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P & not Upper_Arc C c= P holds
Lower_Arc C c= P
let P be Subset of (TOP-REAL 2); ::_thesis: ( P c= C & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P & not Upper_Arc C c= P implies Lower_Arc C c= P )
assume that
A1: P c= C and
A2: P is_an_arc_of p1,p2 and
A3: W-min C in P and
A4: E-max C in P ; ::_thesis: ( Upper_Arc C c= P or Lower_Arc C c= P )
reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A3;
A5: W-min C <> E-max C by TOPREAL5:19;
percases ( LE W-min C, E-max C,P,p1,p2 or LE E-max C, W-min C,P,p1,p2 ) by A2, A3, A4, A5, JORDAN5C:14;
supposeA6: LE W-min C, E-max C,P,p1,p2 ; ::_thesis: ( Upper_Arc C c= P or Lower_Arc C c= P )
set S = Segment (P9,p1,p2,(W-min C),(E-max C));
reconsider S9 = Segment (P9,p1,p2,(W-min C),(E-max C)) as non empty Subset of (TOP-REAL 2) by A6, Th5;
 Segment (P9,p1,p2,(W-min C),(E-max C)) c= P by Th2;
then  Segment (P9,p1,p2,(W-min C),(E-max C)) c= C by A1, XBOOLE_1:1;
then  ( S9 = Lower_Arc C or S9 = Upper_Arc C ) by A2, A5, A6, Th15, Th21;
hence  ( Upper_Arc C c= P or Lower_Arc C c= P ) by Th2; ::_thesis: verum
end;
supposeA7: LE E-max C, W-min C,P,p1,p2 ; ::_thesis: ( Upper_Arc C c= P or Lower_Arc C c= P )
set S = Segment (P9,p1,p2,(E-max C),(W-min C));
reconsider S9 = Segment (P9,p1,p2,(E-max C),(W-min C)) as non empty Subset of (TOP-REAL 2) by A7, Th5;
 Segment (P9,p1,p2,(E-max C),(W-min C)) is_an_arc_of E-max C, W-min C by A2, A5, A7, Th21;
then A8: S9 is_an_arc_of W-min C, E-max C by JORDAN5B:14;
 Segment (P9,p1,p2,(E-max C),(W-min C)) c= P by Th2;
hence  ( Upper_Arc C c= P or Lower_Arc C c= P ) by A1, A8, Th15, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;

theorem :: JORDAN16:23
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & q1 <> q2 holds
ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & q1 <> q2 holds
ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} )
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & q1 <> q2 implies ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} ) )
assume that
A1: P is_an_arc_of p1,p2 and
A2: ( q1 in P & q2 in P ) and
A3: q1 <> p1 and
A4: q1 <> p2 and
A5: q2 <> p1 and
A6: q2 <> p2 and
A7: q1 <> q2 ; ::_thesis: ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} )
percases ( LE q1,q2,P,p1,p2 or LE q2,q1,P,p1,p2 ) by A1, A2, A7, JORDAN5C:14;
supposeA8: LE q1,q2,P,p1,p2 ; ::_thesis: ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} )
set S = Segment (P,p1,p2,q1,q2);
 Segment (P,p1,p2,q1,q2) is_an_arc_of q1,q2 by A1, A7, A8, Th21;
then reconsider S = Segment (P,p1,p2,q1,q2) as non empty Subset of (TOP-REAL 2) by TOPREAL1:1;
take  S ; ::_thesis: ( S is_an_arc_of q1,q2 & S c= P & S misses {p1,p2} )
thus  S is_an_arc_of q1,q2 by A1, A7, A8, Th21; ::_thesis: ( S c= P & S misses {p1,p2} )
thus  S c= P by Th2; ::_thesis: S misses {p1,p2}
now__::_thesis:_not_S_meets_{p1,p2}
A9: S =  {  q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 )  }  by JORDAN6:26;
assume A10: S meets {p1,p2} ; ::_thesis: contradiction
percases ( p1 in S or p2 in S ) by A10, ZFMISC_1:51;
suppose p1 in S ; ::_thesis: contradiction
then  ex q being Point of (TOP-REAL 2) st
( q = p1 & LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) by A9;
hence  contradiction by A1, A3, JORDAN6:54; ::_thesis: verum
end;
suppose p2 in S ; ::_thesis: contradiction
then  ex q being Point of (TOP-REAL 2) st
( q = p2 & LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) by A9;
hence  contradiction by A1, A6, JORDAN6:55; ::_thesis: verum
end;
end;
end;
hence  S misses {p1,p2} ; ::_thesis: verum
end;
supposeA11: LE q2,q1,P,p1,p2 ; ::_thesis: ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} )
set S = Segment (P,p1,p2,q2,q1);
 Segment (P,p1,p2,q2,q1) is_an_arc_of q2,q1 by A1, A7, A11, Th21;
then reconsider S = Segment (P,p1,p2,q2,q1) as non empty Subset of (TOP-REAL 2) by TOPREAL1:1;
take  S ; ::_thesis: ( S is_an_arc_of q1,q2 & S c= P & S misses {p1,p2} )
 S is_an_arc_of q2,q1 by A1, A7, A11, Th21;
hence  S is_an_arc_of q1,q2 by JORDAN5B:14; ::_thesis: ( S c= P & S misses {p1,p2} )
thus  S c= P by Th2; ::_thesis: S misses {p1,p2}
now__::_thesis:_not_S_meets_{p1,p2}
A12: S =  {  q where q is Point of (TOP-REAL 2) : ( LE q2,q,P,p1,p2 & LE q,q1,P,p1,p2 )  }  by JORDAN6:26;
assume A13: S meets {p1,p2} ; ::_thesis: contradiction
percases ( p1 in S or p2 in S ) by A13, ZFMISC_1:51;
suppose p1 in S ; ::_thesis: contradiction
then  ex q being Point of (TOP-REAL 2) st
( q = p1 & LE q2,q,P,p1,p2 & LE q,q1,P,p1,p2 ) by A12;
hence  contradiction by A1, A5, JORDAN6:54; ::_thesis: verum
end;
suppose p2 in S ; ::_thesis: contradiction
then  ex q being Point of (TOP-REAL 2) st
( q = p2 & LE q2,q,P,p1,p2 & LE q,q1,P,p1,p2 ) by A12;
hence  contradiction by A1, A4, JORDAN6:55; ::_thesis: verum
end;
end;
end;
hence  S misses {p1,p2} ; ::_thesis: verum
end;
end;
end;

theorem :: JORDAN16:24
for P being non empty Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & p1 <> q1 holds
Segment (P,p1,p2,p1,q1) is_an_arc_of p1,q1
proof
let P be non empty Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & p1 <> q1 holds
Segment (P,p1,p2,p1,q1) is_an_arc_of p1,q1
let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & q1 in P & p1 <> q1 implies Segment (P,p1,p2,p1,q1) is_an_arc_of p1,q1 )
assume that
A1: P is_an_arc_of p1,p2 and
A2: q1 in P and
A3: p1 <> q1 ; ::_thesis: Segment (P,p1,p2,p1,q1) is_an_arc_of p1,q1
 LE p1,q1,P,p1,p2 by A1, A2, JORDAN5C:10;
hence  Segment (P,p1,p2,p1,q1) is_an_arc_of p1,q1 by A1, A3, Th21; ::_thesis: verum
end;