:: 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;