### The Mizar article:

### A Decomposition of Simple Closed Curves and the Order of Their Points

**by****Yatsuka Nakamura, and****Andrzej Trybulec**

- Received December 19, 1997
Copyright (c) 1997 Association of Mizar Users

- MML identifier: JORDAN6
- [ MML identifier index ]

environ vocabulary ARYTM, PRE_TOPC, EUCLID, TOPMETR, PCOMPS_1, BORSUK_1, RCOMP_1, ARYTM_3, ARYTM_1, RELAT_1, BOOLE, SUBSET_1, ORDINAL2, FUNCT_1, MCART_1, FINSEQ_1, TOPREAL1, RELAT_2, TOPS_2, COMPTS_1, JORDAN5C, JORDAN3, TREAL_1, SEQ_1, PSCOMP_1, TOPREAL2, SEQ_2, METRIC_1, SEQ_4, ABSVALUE, SQUARE_1, FUNCT_5, JORDAN6; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, RCOMP_1, SETWOP_2, STRUCT_0, ABSVALUE, RELAT_1, FUNCT_1, FUNCT_2, TOPREAL1, TOPREAL2, CONNSP_1, JORDAN2B, SQUARE_1, TSEP_1, TOPMETR, PRE_TOPC, TOPS_2, COMPTS_1, BORSUK_1, EUCLID, METRIC_1, PCOMPS_1, SEQ_4, JORDAN5C, TREAL_1, PSCOMP_1; constructors RCOMP_1, ABSVALUE, TOPREAL2, CONNSP_1, JORDAN2B, TSEP_1, TOPS_2, REAL_1, TOPREAL1, SQUARE_1, SETWOP_2, JORDAN5C, TREAL_1, PSCOMP_1, TSP_1, COMPTS_1, YELLOW_8, PARTFUN1, MEMBERED; clusters SUBSET_1, STRUCT_0, FUNCT_1, EUCLID, PRE_TOPC, TOPMETR, METRIC_1, PSCOMP_1, BORSUK_2, TSEP_1, XREAL_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, PRE_TOPC, JORDAN5C, XBOOLE_0; theorems TARSKI, AXIOMS, RCOMP_1, TOPMETR, TOPS_1, METRIC_1, FUNCT_1, FUNCT_2, SEQ_2, FINSEQ_1, REAL_1, ABSVALUE, SPPOL_1, REAL_2, SQUARE_1, PRE_TOPC, TOPS_2, JORDAN1, JORDAN5B, JORDAN5C, TOPREAL1, STRUCT_0, TOPREAL5, SUBSET_1, TREAL_1, PSCOMP_1, RELAT_1, TOPREAL2, JORDAN2B, ENUMSET1, TOPREAL3, JORDAN5A, BORSUK_1, COMPTS_1, CONNSP_1, CONNSP_3, PCOMPS_1, ZFMISC_1, TSEP_1, SEQ_4, RELSET_1, XREAL_0, SPRECT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes DOMAIN_1, COMPLSP1; begin :: Middle Points of Arcs reserve x,y for set; reserve s,r for real number; reserve r1,r2 for Real; reserve n for Nat; reserve p,p3,q,q1,q2,q3 for Point of TOP-REAL 2; canceled; theorem Th2: r<=s implies r <= (r+s)/2 & (r+s)/2 <= s proof assume A1:r<=s; per cases by A1,REAL_1:def 5; suppose r<s; hence thesis by TOPREAL3:3; suppose r=s; hence thesis by XCMPLX_1:65; end; theorem Th3: for TX being non empty TopSpace, P being Subset of TX, A being Subset of TX|P, B being Subset of TX st B is closed & A=B/\P holds A is closed proof let TX be non empty TopSpace,P be Subset of TX, A be Subset of TX|P, B be Subset of TX; assume A1: B is closed & A=B/\P; [#](TX|P)=P by PRE_TOPC:def 10; hence thesis by A1,PRE_TOPC:43; end; theorem Th4: for TX,TY being non empty TopSpace, P being non empty Subset of TY,f being map of TX,TY|P holds f is map of TX,TY & for f2 being map of TX,TY st f2=f & f is continuous holds f2 is continuous proof let TX,TY be non empty TopSpace, P be non empty Subset of TY,f be map of TX,TY|P; A1: the carrier of TY|P = [#](TY|P) by PRE_TOPC:12 .=P by PRE_TOPC:def 10; then f is Function of the carrier of TX,the carrier of TY by FUNCT_2:9; hence f is map of TX,TY ; let f2 be map of TX,TY such that A2: f2=f & f is continuous; let P1 be Subset of TY; assume A3:P1 is closed; reconsider P3=P1/\P as Subset of TY|P by TOPS_2:38; A4: P3 is closed by A3,Th3; A5:f2"P=the carrier of TX by A1,A2,FUNCT_2:48 .=dom f2 by FUNCT_2:def 1; f2"P1 c= dom f2 by RELAT_1:167; then f2"P1=f2"P1 /\ f2"P by A5,XBOOLE_1:28 .=f"P3 by A2,FUNCT_1:137; hence f2"P1 is closed by A2,A4,PRE_TOPC:def 12; end; theorem Th5: for r being real number, P being Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: p`1>=r} holds P is closed proof let r be real number,P be Subset of TOP-REAL 2; assume A1:P={p where p is Point of TOP-REAL 2: p`1>=r}; A2:1 in Seg 2 by FINSEQ_1:3; A3:P`={p where p is Point of TOP-REAL 2: p`1<r} proof A4:P` c= {p where p is Point of TOP-REAL 2: p`1<r} proof let x;assume A5: x in P`; then x in (the carrier of (TOP-REAL 2)) \ P by SUBSET_1:def 5; then A6:x in the carrier of (TOP-REAL 2) & not x in P by XBOOLE_0:def 4; reconsider q=x as Point of TOP-REAL 2 by A5; q`1<r by A1,A6; hence x in {p where p is Point of TOP-REAL 2: p`1<r}; end; {p where p is Point of TOP-REAL 2: p`1<r} c= P` proof let x;assume x in {p where p is Point of TOP-REAL 2: p`1<r}; then consider p being Point of TOP-REAL 2 such that A7:p=x & p`1<r; now assume x in {q where q is Point of TOP-REAL 2: q`1>=r}; then consider q being Point of TOP-REAL 2 such that A8:q=x & q`1>=r; thus contradiction by A7,A8; end; then x in (the carrier of TOP-REAL 2) \P by A1,A7,XBOOLE_0:def 4; hence x in P` by SUBSET_1:def 5; end; hence thesis by A4,XBOOLE_0:def 10; end; A9: P`={p where p is Point of TOP-REAL 2: r>Proj(p,1)} proof A10: P`c= {p where p is Point of TOP-REAL 2: r>Proj(p,1)} proof let x;assume x in P`; then consider p being Point of TOP-REAL 2 such that A11:p=x & p`1<r by A3; Proj(p,1)<r by A11,JORDAN2B:35; hence thesis by A11; end; {p where p is Point of TOP-REAL 2: r>Proj(p,1)} c= P` proof let x;assume x in {p where p is Point of TOP-REAL 2: r>Proj(p,1)}; then consider q being Point of TOP-REAL 2 such that A12:q=x & r>Proj(q,1); q`1<r by A12,JORDAN2B:35; hence x in P` by A3,A12; end; hence thesis by A10,XBOOLE_0:def 10; end; reconsider P1 = P` as Subset of TOP-REAL 2; P1 is open by A2,A9,JORDAN2B:16; hence P is closed by TOPS_1:29; end; theorem Th6: for r being real number, P being Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: p`1<=r} holds P is closed proof let r be real number, P be Subset of TOP-REAL 2; assume A1:P={p where p is Point of TOP-REAL 2: p`1<=r}; A2:1 in Seg 2 by FINSEQ_1:3; A3:P`={p where p is Point of TOP-REAL 2: p`1>r} proof A4:P` c= {p where p is Point of TOP-REAL 2: p`1>r} proof let x;assume A5: x in P`; then x in (the carrier of (TOP-REAL 2)) \ P by SUBSET_1:def 5; then A6:x in the carrier of (TOP-REAL 2) & not x in P by XBOOLE_0:def 4; reconsider q=x as Point of TOP-REAL 2 by A5; q`1>r by A1,A6; hence x in {p where p is Point of TOP-REAL 2: p`1>r}; end; {p where p is Point of TOP-REAL 2: p`1>r} c= P` proof let x;assume x in {p where p is Point of TOP-REAL 2: p`1>r}; then consider p being Point of TOP-REAL 2 such that A7:p=x & p`1>r; now assume x in {q where q is Point of TOP-REAL 2: q`1<=r}; then consider q being Point of TOP-REAL 2 such that A8:q=x & q`1<=r; thus contradiction by A7,A8; end; then x in (the carrier of TOP-REAL 2) \P by A1,A7,XBOOLE_0:def 4; hence x in P` by SUBSET_1:def 5; end; hence thesis by A4,XBOOLE_0:def 10; end; A9: P`={p where p is Point of TOP-REAL 2: r<Proj(p,1)} proof A10: P`c= {p where p is Point of TOP-REAL 2: r<Proj(p,1)} proof let x;assume x in P`; then consider p being Point of TOP-REAL 2 such that A11:p=x & p`1>r by A3; Proj(p,1)>r by A11,JORDAN2B:35; hence thesis by A11; end; {p where p is Point of TOP-REAL 2: r<Proj(p,1)} c= P` proof let x;assume x in {p where p is Point of TOP-REAL 2: r<Proj(p,1)}; then consider q being Point of TOP-REAL 2 such that A12:q=x & r<Proj(q,1); q`1>r by A12,JORDAN2B:35; hence x in P` by A3,A12; end; hence thesis by A10,XBOOLE_0:def 10; end; reconsider P1 = P` as Subset of TOP-REAL 2; P1 is open by A2,A9,JORDAN2B:17; hence P is closed by TOPS_1:29; end; theorem Th7: for r being real number,P being Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: p`1=r} holds P is closed proof let r be real number,P be Subset of TOP-REAL 2; assume A1:P={p where p is Point of TOP-REAL 2: p`1=r}; defpred P[Point of TOP-REAL 2] means $1`1>=r; {p where p is Element of TOP-REAL 2 : P[p]} is Subset of TOP-REAL 2 from SubsetD; then reconsider P1={p where p is Point of TOP-REAL 2: p`1>=r} as Subset of TOP-REAL 2; A2:P1 is closed by Th5; defpred Q[Point of TOP-REAL 2] means $1`1<=r; {p where p is Element of TOP-REAL 2 : Q[p]} is Subset of TOP-REAL 2 from SubsetD; then reconsider P2={p where p is Point of TOP-REAL 2: p`1<=r} as Subset of TOP-REAL 2; A3:P2 is closed by Th6; P=P1 /\ P2 proof A4:P c= P1 /\ P2 proof let x;assume x in P; then ex p being Point of TOP-REAL 2 st p=x & p`1=r by A1; then x in P1 & x in P2; hence x in P1 /\ P2 by XBOOLE_0:def 3; end; P1 /\ P2 c= P proof let x;assume x in P1 /\ P2; then A5:x in P1 & x in P2 by XBOOLE_0:def 3; then consider q1 being Point of TOP-REAL 2 such that A6:q1=x & q1`1>=r; consider q2 being Point of TOP-REAL 2 such that A7:q2=x & q2`1<=r by A5; q1`1=r by A6,A7,AXIOMS:21; hence x in P by A1,A6; end; hence thesis by A4,XBOOLE_0:def 10; end; hence P is closed by A2,A3,TOPS_1:35; end; theorem Th8: for r being real number, P being Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: p`2>=r} holds P is closed proof let r be real number, P be Subset of TOP-REAL 2; assume A1:P={p where p is Point of TOP-REAL 2: p`2>=r}; A2:2 in Seg 2 by FINSEQ_1:3; A3:P`={p where p is Point of TOP-REAL 2: p`2<r} proof A4:P` c= {p where p is Point of TOP-REAL 2: p`2<r} proof let x;assume A5: x in P`; then x in (the carrier of (TOP-REAL 2)) \ P by SUBSET_1:def 5; then A6:x in the carrier of (TOP-REAL 2) & not x in P by XBOOLE_0:def 4; reconsider q=x as Point of TOP-REAL 2 by A5; q`2<r by A1,A6; hence x in {p where p is Point of TOP-REAL 2: p`2<r}; end; {p where p is Point of TOP-REAL 2: p`2<r} c= P` proof let x;assume x in {p where p is Point of TOP-REAL 2: p`2<r}; then consider p being Point of TOP-REAL 2 such that A7:p=x & p`2<r; now assume x in {q where q is Point of TOP-REAL 2: q`2>=r}; then consider q being Point of TOP-REAL 2 such that A8:q=x & q`2>=r; thus contradiction by A7,A8; end; then x in (the carrier of TOP-REAL 2) \P by A1,A7,XBOOLE_0:def 4; hence x in P` by SUBSET_1:def 5; end; hence thesis by A4,XBOOLE_0:def 10; end; A9: P`={p where p is Point of TOP-REAL 2: r>Proj(p,2)} proof A10: P`c= {p where p is Point of TOP-REAL 2: r>Proj(p,2)} proof let x;assume x in P`; then consider p being Point of TOP-REAL 2 such that A11:p=x & p`2<r by A3; Proj(p,2)<r by A11,JORDAN2B:35; hence thesis by A11; end; {p where p is Point of TOP-REAL 2: r>Proj(p,2)} c= P` proof let x;assume x in {p where p is Point of TOP-REAL 2: r>Proj(p,2)}; then consider q being Point of TOP-REAL 2 such that A12:q=x & r>Proj(q,2); q`2<r by A12,JORDAN2B:35; hence x in P` by A3,A12; end; hence thesis by A10,XBOOLE_0:def 10; end; reconsider P1 = P` as Subset of TOP-REAL 2; P1 is open by A2,A9,JORDAN2B:16; hence P is closed by TOPS_1:29; end; theorem Th9: for r being real number, P being Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: p`2<=r} holds P is closed proof let r be real number, P be Subset of TOP-REAL 2; assume A1:P={p where p is Point of TOP-REAL 2: p`2<=r}; A2:2 in Seg 2 by FINSEQ_1:3; A3:P`={p where p is Point of TOP-REAL 2: p`2>r} proof A4:P` c= {p where p is Point of TOP-REAL 2: p`2>r} proof let x;assume A5: x in P`; then x in (the carrier of (TOP-REAL 2)) \ P by SUBSET_1:def 5; then A6:x in the carrier of (TOP-REAL 2) & not x in P by XBOOLE_0:def 4; reconsider q=x as Point of TOP-REAL 2 by A5; q`2>r by A1,A6; hence x in {p where p is Point of TOP-REAL 2: p`2>r}; end; {p where p is Point of TOP-REAL 2: p`2>r} c= P` proof let x;assume x in {p where p is Point of TOP-REAL 2: p`2>r}; then consider p being Point of TOP-REAL 2 such that A7:p=x & p`2>r; now assume x in {q where q is Point of TOP-REAL 2: q`2<=r}; then consider q being Point of TOP-REAL 2 such that A8:q=x & q`2<=r; thus contradiction by A7,A8; end; then x in (the carrier of TOP-REAL 2) \P by A1,A7,XBOOLE_0:def 4; hence x in P` by SUBSET_1:def 5; end; hence thesis by A4,XBOOLE_0:def 10; end; A9: P`={p where p is Point of TOP-REAL 2: r<Proj(p,2)} proof A10: P`c= {p where p is Point of TOP-REAL 2: r<Proj(p,2)} proof let x;assume x in P`; then consider p being Point of TOP-REAL 2 such that A11:p=x & p`2>r by A3; Proj(p,2)>r by A11,JORDAN2B:35; hence thesis by A11; end; {p where p is Point of TOP-REAL 2: r<Proj(p,2)} c= P` proof let x;assume x in {p where p is Point of TOP-REAL 2: r<Proj(p,2)}; then consider q being Point of TOP-REAL 2 such that A12:q=x & r<Proj(q,2); q`2>r by A12,JORDAN2B:35; hence x in P` by A3,A12; end; hence thesis by A10,XBOOLE_0:def 10; end; reconsider P1 = P` as Subset of TOP-REAL 2; P1 is open by A2,A9,JORDAN2B:17; hence P is closed by TOPS_1:29; end; theorem Th10: for r being real number, P being Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: p`2=r} holds P is closed proof let r be real number, P be Subset of TOP-REAL 2; assume A1:P={p where p is Point of TOP-REAL 2: p`2=r}; defpred P[Point of TOP-REAL 2] means $1`2>=r; {p where p is Element of TOP-REAL 2 : P[p]} is Subset of TOP-REAL 2 from SubsetD; then reconsider P1={p where p is Point of TOP-REAL 2: p`2>=r} as Subset of TOP-REAL 2; A2:P1 is closed by Th8; defpred Q[Point of TOP-REAL 2] means $1`2<=r; {p where p is Element of TOP-REAL 2 : Q[p]} is Subset of TOP-REAL 2 from SubsetD; then reconsider P2={p where p is Point of TOP-REAL 2: p`2<=r} as Subset of TOP-REAL 2; A3:P2 is closed by Th9; P=P1 /\ P2 proof A4:P c= P1 /\ P2 proof let x;assume x in P; then consider p being Point of TOP-REAL 2 such that A5:p=x & p`2=r by A1 ; x in P1 & x in P2 by A5; hence x in P1 /\ P2 by XBOOLE_0:def 3; end; P1 /\ P2 c= P proof let x;assume x in P1 /\ P2; then A6:x in P1 & x in P2 by XBOOLE_0:def 3; then consider q1 being Point of TOP-REAL 2 such that A7:q1=x & q1`2>=r; consider q2 being Point of TOP-REAL 2 such that A8:q2=x & q2`2<=r by A6; q1`2=r by A7,A8,AXIOMS:21; hence x in P by A1,A7; end; hence thesis by A4,XBOOLE_0:def 10; end; hence P is closed by A2,A3,TOPS_1:35; end; theorem Th11: for P being Subset of TOP-REAL n, p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 holds P is connected proof let P be Subset of TOP-REAL n, p1,p2 be Point of TOP-REAL n; assume A1: P is_an_arc_of p1,p2; then consider f being map of I[01], (TOP-REAL n)|P such that A2: f is_homeomorphism & f.0 = p1 & f.1 = p2 by TOPREAL1:def 2; reconsider P' = P as non empty Subset of TOP-REAL n by A1,TOPREAL1:4; A3: f is continuous map of I[01],(TOP-REAL n)|P' by A2,TOPS_2:def 5; A4: [#]I[01] is connected by CONNSP_1:28,TREAL_1:22; A5:rng f=[#]((TOP-REAL n)|P) by A2,TOPS_2:def 5; A6:[#]((TOP-REAL n)|P)=P by PRE_TOPC:def 10; dom f=[#]I[01] by A2,TOPS_2:def 5; then A7:P=f.:([#]I[01]) by A5,A6,RELAT_1:146; f.:([#]I[01]) is connected by A3,A4,TOPREAL5:5; hence P is connected by A7,CONNSP_3:34; end; theorem Th12: for P being Subset of TOP-REAL 2,p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds P is closed proof let P be Subset of TOP-REAL 2,p1,p2 be Point of TOP-REAL 2; assume A1: P is_an_arc_of p1,p2; reconsider P00=P as Subset of TOP-REAL 2; P00 is compact by A1,JORDAN5A:1; hence P is closed by COMPTS_1:16; end; theorem Th13: for P being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds ex q being Point of TOP-REAL 2 st q in P & q `1 = (p1 `1+p2 `1)/2 proof let P be Subset of (TOP-REAL 2), p1,p2 be Point of TOP-REAL 2; assume A1: P is_an_arc_of p1,p2; then A2:p1 in P by TOPREAL1:4; reconsider P' = P as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:4; consider f being map of I[01], (TOP-REAL 2)|P' such that A3:f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2; A4:f is continuous by A3,TOPS_2:def 5; consider h being map of TOP-REAL 2,R^1 such that A5:for p being Element of TOP-REAL 2 holds h.p=Proj(p,1) by JORDAN2B:1; 1 in Seg 2 by FINSEQ_1:3; then A6:h is continuous by A5,JORDAN2B:22; A7: the carrier of (TOP-REAL 2)|P = [#]((TOP-REAL 2)|P) by PRE_TOPC:12 .=P' by PRE_TOPC:def 10; then A8:f is Function of the carrier of I[01],the carrier of TOP-REAL 2 by FUNCT_2:9; then reconsider f1=f as map of I[01],TOP-REAL 2 ; A9:f1 is continuous by A4,Th4; h*f is Function of the carrier of I[01],the carrier of R^1 by A8,FUNCT_2:19; then reconsider g= h*f as map of I[01],R^1 ; A10:g is continuous by A6,A9,TOPS_2:58; A11:dom f=[.0,1.] by BORSUK_1:83,FUNCT_2:def 1; then A12:0 in dom f by TOPREAL5:1; A13:1 in dom f by A11,TOPREAL5:1; A14:g.0 =h.(f.0) by A12,FUNCT_1:23 .=Proj(p1,1) by A3,A5 .=p1`1 by JORDAN2B:35; A15:g.1 =h.(f.1) by A13,FUNCT_1:23 .=Proj(p2,1) by A3,A5 .=p2`1 by JORDAN2B:35; per cases; suppose g.0<>g.1; then consider r1 being Real such that A16:0<r1 & r1<1 & g.r1=(p1`1+p2`1)/2 by A10,A14,A15,TOPREAL5:15; A17:r1 in [.0,1.] by A16,TOPREAL5:1; A18:r1 in the carrier of I[01] by A16,BORSUK_1:83,TOPREAL5:1; then reconsider q1=f.r1 as Point of TOP-REAL 2 by A8,FUNCT_2:7; A19:f.r1 in P by A7,A18,FUNCT_2:7; g.r1= h.(f.r1) by A11,A17,FUNCT_1:23 .=Proj(q1,1) by A5 .=q1`1 by JORDAN2B:35; hence thesis by A16,A19; suppose g.0=g.1; then p1 `1 = (p1 `1+p2 `1)/2 by A14,A15,XCMPLX_1:65; hence thesis by A2; end; theorem Th14: for P,Q being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & Q={q:q`1=(p1`1+p2`1)/2} holds P meets Q & P /\ Q is closed proof let P,Q be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; reconsider W = P as Subset of TOP-REAL 2; assume A1:P is_an_arc_of p1,p2 & Q={q:q`1=(p1`1+p2`1)/2}; consider f being map of TOP-REAL 2,R^1 such that A2: for p being Element of TOP-REAL 2 holds f.p=Proj(p,1) by JORDAN2B:1; reconsider P' = P as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:4; 1 in Seg 2 by FINSEQ_1:3; then A3:f is continuous by A2,JORDAN2B:22; A4:dom f=the carrier of TOP-REAL 2 by FUNCT_2:def 1; [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 10; then A5:the carrier of (TOP-REAL 2)|P'=P' by PRE_TOPC:12; A6:dom (f|P)=(the carrier of TOP-REAL 2)/\P by A4,RELAT_1:90 .=P by XBOOLE_1:28; rng (f|P) c= rng f by FUNCT_1:76; then rng (f|P) c= the carrier of R^1 by XBOOLE_1:1; then f|P is Function of the carrier of (TOP-REAL 2)|P,the carrier of R^1 by A5,A6,FUNCT_2:def 1,RELSET_1:11; then reconsider g=f|P as map of (TOP-REAL 2)|P,R^1 ; reconsider g as continuous map of (TOP-REAL 2)|P',R^1 by A3,TOPMETR:10; A7:p1 in P & p2 in P by A1,TOPREAL1:4; reconsider p1'=p1, p2'=p2 as Point of (TOP-REAL 2)|P by A1,A5,TOPREAL1:4; A8:g.p1'=f.p1 by A7,FUNCT_1:72 .=Proj(p1,1) by A2 .=p1`1 by JORDAN2B:35; A9: g.p2'=f.p2 by A7,FUNCT_1:72 .=Proj(p2,1) by A2 .=p2`1 by JORDAN2B:35; W is connected by A1,Th11; then A10:(TOP-REAL 2)|P is connected by CONNSP_1:def 3; A11: now per cases; case p1`1<=p2`1; then p1`1<=(p1`1+p2`1)/2 & (p1`1+p2`1)/2<=p2`1 by Th2; then consider xc being Point of (TOP-REAL 2)|P such that A12:g.xc=(p1`1+p2`1)/2 by A8,A9,A10,TOPREAL5:10; xc in P by A5; then reconsider pc=xc as Point of TOP-REAL 2; g.xc =f.xc by A5,FUNCT_1:72 .=Proj(pc,1) by A2 .=pc`1 by JORDAN2B:35; then xc in Q by A1,A12; hence P meets Q by A5,XBOOLE_0:3; case p1`1>p2`1; then p2`1<=(p1`1+p2`1)/2 & (p1`1+p2`1)/2<=p1`1 by Th2; then consider xc being Point of (TOP-REAL 2)|P such that A13:g.xc=(p1`1+p2`1)/2 by A8,A9,A10,TOPREAL5:10; xc in P by A5; then reconsider pc=xc as Point of TOP-REAL 2; g.xc =f.xc by A5,FUNCT_1:72 .=Proj(pc,1) by A2 .=pc`1 by JORDAN2B:35; then xc in Q by A1,A13; hence P meets Q by A5,XBOOLE_0:3; end; reconsider P1 = P, Q1 = Q as Subset of TOP-REAL 2; A14:P1 is closed by A1,Th12; Q1 is closed by A1,Th7; hence thesis by A11,A14,TOPS_1:35; end; theorem Th15: for P,Q being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & Q={q:q`2=(p1`2+p2`2)/2} holds P meets Q & P /\ Q is closed proof let P,Q1 be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; assume A1:P is_an_arc_of p1,p2 & Q1={q:q`2=(p1`2+p2`2)/2}; consider f being map of TOP-REAL 2,R^1 such that A2: for p being Element of TOP-REAL 2 holds f.p=Proj(p,2) by JORDAN2B:1; reconsider P' = P as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:4; 2 in Seg 2 by FINSEQ_1:3; then A3:f is continuous by A2,JORDAN2B:22; A4:dom f=the carrier of TOP-REAL 2 by FUNCT_2:def 1; [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 10; then A5:the carrier of (TOP-REAL 2)|P'=P' by PRE_TOPC:12; A6:dom (f|P)=(the carrier of TOP-REAL 2)/\P by A4,RELAT_1:90 .=P by XBOOLE_1:28; rng (f|P) c= rng f by FUNCT_1:76; then rng (f|P) c= the carrier of R^1 by XBOOLE_1:1; then f|P is Function of the carrier of (TOP-REAL 2)|P,the carrier of R^1 by A5,A6,FUNCT_2:def 1,RELSET_1:11; then reconsider g=f|P as map of (TOP-REAL 2)|P,R^1 ; reconsider g as continuous map of (TOP-REAL 2)|P',R^1 by A3,TOPMETR:10; A7:p1 in P & p2 in P by A1,TOPREAL1:4; reconsider p1'=p1, p2'=p2 as Point of (TOP-REAL 2)|P by A1,A5,TOPREAL1:4; A8:g.p1'=f.p1 by A7,FUNCT_1:72 .=Proj(p1,2) by A2 .=p1`2 by JORDAN2B:35; A9: g.p2'=f.p2 by A7,FUNCT_1:72 .=Proj(p2,2) by A2 .=p2`2 by JORDAN2B:35; reconsider W = P as Subset of TOP-REAL 2; W is connected by A1,Th11; then A10:(TOP-REAL 2)|P is connected by CONNSP_1:def 3; A11: now per cases; case p1`2<=p2`2; then p1`2<=(p1`2+p2`2)/2 & (p1`2+p2`2)/2<=p2`2 by Th2; then consider xc being Point of (TOP-REAL 2)|P such that A12:g.xc=(p1`2+p2`2)/2 by A8,A9,A10,TOPREAL5:10; xc in P by A5; then reconsider pc=xc as Point of TOP-REAL 2; g.xc =f.xc by A5,FUNCT_1:72 .=Proj(pc,2) by A2 .=pc`2 by JORDAN2B:35; then xc in Q1 by A1,A12; hence P meets Q1 by A5,XBOOLE_0:3; case p1`2>p2`2; then p2`2<=(p1`2+p2`2)/2 & (p1`2+p2`2)/2<=p1`2 by Th2; then consider xc being Point of (TOP-REAL 2)|P such that A13:g.xc=(p1`2+p2`2)/2 by A8,A9,A10,TOPREAL5:10; xc in P by A5; then reconsider pc=xc as Point of TOP-REAL 2; g.xc =f.xc by A5,FUNCT_1:72 .=Proj(pc,2) by A2 .=pc`2 by JORDAN2B:35; then xc in Q1 by A1,A13; hence P meets Q1 by A5,XBOOLE_0:3; end; reconsider P1 = P, Q2 = Q1 as Subset of TOP-REAL 2; A14:P1 is closed by A1,Th12; Q2 is closed by A1,Th10; hence thesis by A11,A14,TOPS_1:35; end; definition let P be non empty Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; func x_Middle(P,p1,p2) -> Point of TOP-REAL 2 means :Def1: for Q being Subset of TOP-REAL 2 st Q={q:q`1=(p1`1+p2`1)/2} holds it=First_Point(P,p1,p2,Q); existence proof {q:q`1=(p1`1+p2`1)/2} c= the carrier of TOP-REAL 2 proof let x;assume x in {q:q`1=(p1`1+p2`1)/2}; then consider q being Point of TOP-REAL 2 such that A1:q=x & (q`1=(p1`1+p2`1)/2); thus x in the carrier of TOP-REAL 2 by A1; end; then reconsider Q1={q:q`1=(p1`1+p2`1)/2} as Subset of TOP-REAL 2; reconsider q2=First_Point(P,p1,p2,Q1) as Point of TOP-REAL 2; for Q being Subset of TOP-REAL 2 st Q={q:q`1=(p1`1+p2`1)/2} holds q2=First_Point(P,p1,p2,Q); hence thesis; end; uniqueness proof let q3,q4 be Point of TOP-REAL 2; assume A2:(for Q1 being Subset of TOP-REAL 2 st Q1={q1:q1`1=(p1`1+p2`1)/2} holds q3=First_Point(P,p1,p2,Q1)) & (for Q2 being Subset of TOP-REAL 2 st Q2={q2:q2`1=(p1`1+p2`1)/2} holds q4=First_Point(P,p1,p2,Q2)); {q1:q1`1=(p1`1+p2`1)/2} c= the carrier of TOP-REAL 2 proof let x;assume x in {q1:q1`1=(p1`1+p2`1)/2}; then consider q being Point of TOP-REAL 2 such that A3:q=x & (q`1=(p1`1+p2`1)/2); thus x in the carrier of TOP-REAL 2 by A3; end; then reconsider Q3={q2:q2`1=(p1`1+p2`1)/2} as Subset of TOP-REAL 2; q3=First_Point(P,p1,p2,Q3) by A2; hence q3=q4 by A2; end; end; definition let P be non empty Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; func y_Middle(P,p1,p2) -> Point of TOP-REAL 2 means :Def2: for Q being Subset of TOP-REAL 2 st Q={q:q`2=(p1`2+p2`2)/2} holds it=First_Point(P,p1,p2,Q); existence proof {q:q`2=(p1`2+p2`2)/2} c= the carrier of TOP-REAL 2 proof let x;assume x in {q:q`2=(p1`2+p2`2)/2}; then consider q being Point of TOP-REAL 2 such that A1:q=x & (q`2=(p1`2+p2`2)/2); thus x in the carrier of TOP-REAL 2 by A1; end; then reconsider Q1={q:q`2=(p1`2+p2`2)/2} as Subset of TOP-REAL 2; reconsider q2=First_Point(P,p1,p2,Q1) as Point of TOP-REAL 2; for Q being Subset of TOP-REAL 2 st Q={q:q`2=(p1`2+p2`2)/2} holds q2=First_Point(P,p1,p2,Q); hence thesis; end; uniqueness proof let q3,q4 be Point of TOP-REAL 2; assume A2:(for Q1 being Subset of TOP-REAL 2 st Q1={q1:q1`2=(p1`2+p2`2)/2} holds q3=First_Point(P,p1,p2,Q1)) & (for Q2 being Subset of TOP-REAL 2 st Q2={q2:q2`2=(p1`2+p2`2)/2} holds q4=First_Point(P,p1,p2,Q2)); {q1:q1`2=(p1`2+p2`2)/2} c= the carrier of TOP-REAL 2 proof let x;assume x in {q1:q1`2=(p1`2+p2`2)/2}; then consider q being Point of TOP-REAL 2 such that A3:q=x & (q`2=(p1`2+p2`2)/2); thus x in the carrier of TOP-REAL 2 by A3; end; then reconsider Q3={q2:q2`2=(p1`2+p2`2)/2} as Subset of TOP-REAL 2; q3=First_Point(P,p1,p2,Q3) by A2; hence q3=q4 by A2; end; end; theorem for P being non empty Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds x_Middle(P,p1,p2) in P & y_Middle(P,p1,p2) in P proof let P be non empty Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; assume A1: P is_an_arc_of p1,p2; deffunc F(Point of TOP-REAL 2)=$1; defpred P[Point of TOP-REAL 2] means $1`1=(p1`1+p2`1)/2; reconsider Q={F(q):P[q]} as Subset of TOP-REAL 2 from SubsetFD; A2:x_Middle(P,p1,p2)=First_Point(P,p1,p2,Q) by Def1; P meets Q & P /\ Q is closed by A1,Th14; then A3: x_Middle(P,p1,p2) in P /\ Q by A1,A2,JORDAN5C:def 1; defpred Q[Point of TOP-REAL 2] means $1`2=(p1`2+p2`2)/2; reconsider Q2={F(q):Q[q]} as Subset of TOP-REAL 2 from SubsetFD; A4: y_Middle(P,p1,p2)=First_Point(P,p1,p2,Q2) by Def2; P meets Q2 & P /\ Q2 is closed by A1,Th15; then y_Middle(P,p1,p2) in P /\ Q2 by A1,A4,JORDAN5C:def 1; hence thesis by A3,XBOOLE_0:def 3; end; theorem for P being non empty Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds p1=x_Middle(P,p1,p2) iff p1`1=p2`1 proof let P be non empty Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; assume A1: P is_an_arc_of p1,p2; A2:now assume A3:p1=x_Middle(P,p1,p2); deffunc F(Point of TOP-REAL 2)=$1; defpred P[Point of TOP-REAL 2] means $1`1=(p1`1+p2`1)/2; reconsider Q1={F(q):P[q]} as Subset of TOP-REAL 2 from SubsetFD; A4:P meets Q1 & P /\ Q1 is closed by A1,Th14; x_Middle(P,p1,p2)=First_Point(P,p1,p2,Q1) by Def1; then p1 in P /\ Q1 by A1,A3,A4,JORDAN5C:def 1; then p1 in Q1 by XBOOLE_0:def 3; then ex q st q=p1 & q`1=(p1`1+p2`1)/2; hence p1`1=p2`1 by XCMPLX_1:67; end; now assume p1`1=p2`1; then A5:p1`1=(p1`1+p2`1)/2 by XCMPLX_1:65; for Q being Subset of TOP-REAL 2 st Q={q:q`1=(p1`1+p2`1)/2} holds p1=First_Point(P,p1,p2,Q) proof let Q be Subset of TOP-REAL 2; assume A6: Q={q:q`1=(p1`1+p2`1)/2}; then A7:p1 in Q by A5; P meets Q & P /\ Q is closed by A1,A6,Th14; hence p1=First_Point(P,p1,p2,Q) by A1,A7,JORDAN5C:3; end; hence p1=x_Middle(P,p1,p2) by Def1; end; hence thesis by A2; end; theorem for P being non empty Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds p1=y_Middle(P,p1,p2) iff p1`2=p2`2 proof let P be non empty Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; assume A1: P is_an_arc_of p1,p2; A2:now assume A3:p1=y_Middle(P,p1,p2); deffunc F(Point of TOP-REAL 2)=$1; defpred P[Point of TOP-REAL 2] means $1`2=(p1`2+p2`2)/2; reconsider Q1={F(q):P[q]} as Subset of TOP-REAL 2 from SubsetFD; A4:P meets Q1 & P /\ Q1 is closed by A1,Th15; y_Middle(P,p1,p2)=First_Point(P,p1,p2,Q1) by Def2; then p1 in P /\ Q1 by A1,A3,A4,JORDAN5C:def 1; then p1 in Q1 by XBOOLE_0:def 3; then consider q such that A5:q=p1 & q`2=(p1`2+p2`2)/2; thus p1`2=p2`2 by A5,XCMPLX_1:67; end; now assume p1`2=p2`2; then A6:p1`2=(p1`2+p2`2)/2 by XCMPLX_1:65; for Q being Subset of TOP-REAL 2 st Q={q:q`2=(p1`2+p2`2)/2} holds p1=First_Point(P,p1,p2,Q) proof let Q be Subset of TOP-REAL 2; assume A7: Q={q:q`2=(p1`2+p2`2)/2}; then A8:p1 in Q by A6; P meets Q & P /\ Q is closed by A1,A7,Th15; hence p1=First_Point(P,p1,p2,Q) by A1,A8,JORDAN5C:3; end; hence p1=y_Middle(P,p1,p2) by Def2; end; hence thesis by A2; end; begin ::Segments of Arcs theorem Th19: for P being Subset of TOP-REAL 2, p1,p2,q1,q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 holds LE q2,q1,P,p2,p1 proof let P be Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2; assume A1: P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2; hence q2 in P & q1 in P by JORDAN5C:def 3; reconsider P' = P as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:4; let f be map of I[01], (TOP-REAL 2)|P, s1, s2 be Real; assume A2:f is_homeomorphism & f.0 = p2 & f.1 = p1 & f.s1 = q2 & 0 <= s1 & s1 <= 1 & f.s2 = q1 & 0 <= s2 & s2 <= 1; then A3: 1-0>=1-s1 by REAL_1:92; A4: 1-0>=1-s2 by A2,REAL_1:92; A5: 1-1<=1-s1 by A2,REAL_1:92; A6: 1-1<=1-s2 by A2,REAL_1:92; set Ex = L[01]((0,1)(#),(#)(0,1)); A7: Ex is_homeomorphism by TREAL_1:21; set g = f * Ex; A8: Ex.(0,1)(#) = 0 by BORSUK_1:def 17,TREAL_1:8,12; A9: Ex.(#)(0,1) = 1 by BORSUK_1:def 18,TREAL_1:8,12; dom f = [#]I[01] by A2,TOPS_2:def 5; then A10: rng Ex = dom f by A7,TOPMETR:27,TOPS_2:def 5; then A11: dom g = dom Ex by RELAT_1:46; rng g = rng f by A10,RELAT_1:47; then A12: rng g = [#] ((TOP-REAL 2) | P) by A2,TOPS_2:def 5; dom g = [#]I[01] by A7,A11,TOPMETR:27,TOPS_2:def 5; then A13: dom g = the carrier of I[01] & rng g = the carrier of ((TOP-REAL 2) | P) by A12,PRE_TOPC:12; then g is Function of the carrier of I[01], the carrier of ((TOP-REAL 2)|P') by FUNCT_2:def 1,RELSET_1:11; then reconsider g as map of I[01], (TOP-REAL 2)|P' ; A14: g is_homeomorphism by A2,A7,TOPMETR:27,TOPS_2:71; A15:(1-s1) in dom g & (1-s2) in dom g by A3,A4,A5,A6,A13,JORDAN5A:2; A16: g.0 = p1 by A2,A9,A13,BORSUK_1:def 17,FUNCT_1:22,TREAL_1:8; A17: g.1 = p2 by A2,A8,A13,BORSUK_1:def 18,FUNCT_1:22,TREAL_1:8; reconsider qs1=1-s1,qs2=1-s2 as Point of Closed-Interval-TSpace(0,1) by A3,A4,A5,A6,JORDAN5A:2,TOPMETR:27; A18: Ex.qs1 = (1-(1-s1))*1+(1-s1)*0 by BORSUK_1:def 17,def 18,TREAL_1:8,def 3 .=s1 by XCMPLX_1:18; A19: Ex.qs2 = (1-(1-s2))*1+(1-s2)*0 by BORSUK_1:def 17,def 18,TREAL_1:8,def 3 .=s2 by XCMPLX_1:18; A20: g.(1-s1) = q2 by A2,A15,A18,FUNCT_1:22; g.(1-s2) = q1 by A2,A15,A19,FUNCT_1:22; then 1-s2<=1-s1 by A1,A3,A4,A5,A6,A14,A16,A17,A20,JORDAN5C:def 3; then s1<=1-(1-s2) by REAL_2:165; hence s1<=s2 by XCMPLX_1:18; end; definition let P be Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2; func L_Segment(P,p1,p2,q1) -> Subset of TOP-REAL 2 equals :Def3: {q : LE q,q1,P,p1,p2}; coherence proof {q : LE q,q1,P,p1,p2} c= the carrier of TOP-REAL 2 proof let x;assume x in {q : LE q,q1,P,p1,p2}; then consider q such that A1:q=x & LE q,q1,P,p1,p2; thus x in the carrier of TOP-REAL 2 by A1; end; hence {q : LE q,q1,P,p1,p2} is Subset of TOP-REAL 2; end; end; definition let P be Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2; func R_Segment(P,p1,p2,q1) -> Subset of TOP-REAL 2 equals :Def4: {q: LE q1,q,P,p1,p2}; coherence proof {q : LE q1,q,P,p1,p2} c= the carrier of TOP-REAL 2 proof let x;assume x in {q : LE q1,q,P,p1,p2}; then consider q such that A1:q=x & LE q1,q,P,p1,p2; thus x in the carrier of TOP-REAL 2 by A1; end; hence {q : LE q1,q,P,p1,p2} is Subset of TOP-REAL 2; end; end; theorem Th20: for P being Subset of TOP-REAL 2, p1,p2,q1 being Point of TOP-REAL 2 holds L_Segment(P,p1,p2,q1) c= P proof let P be Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2; let x;assume x in L_Segment(P,p1,p2,q1); then x in {q: LE q,q1,P,p1,p2} by Def3; then ex q st q=x & LE q,q1,P,p1,p2; hence x in P by JORDAN5C:def 3; end; theorem Th21: for P being Subset of TOP-REAL 2, p1,p2,q1 being Point of TOP-REAL 2 holds R_Segment(P,p1,p2,q1) c= P proof let P be Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2; let x;assume x in R_Segment(P,p1,p2,q1); then x in {q: LE q1,q,P,p1,p2} by Def4; then ex q st q=x & LE q1,q,P,p1,p2; hence x in P by JORDAN5C:def 3; end; theorem for P being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds L_Segment(P,p1,p2,p1)={p1} proof let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; assume A1: P is_an_arc_of p1,p2; then A2:p1 in P by TOPREAL1:4; thus L_Segment(P,p1,p2,p1) c= {p1} proof let x;assume x in L_Segment(P,p1,p2,p1); then x in {q: LE q,p1,P,p1,p2} by Def3; then consider q such that A3:q=x & LE q,p1,P,p1,p2; q in P by A3,JORDAN5C:def 3; then LE p1,q,P,p1,p2 & LE q,p2,P,p1,p2 by A1,JORDAN5C:10; then q=p1 by A1,A3,JORDAN5C:12; hence x in {p1} by A3,TARSKI:def 1; end; let x;assume x in {p1}; then A4:x=p1 by TARSKI:def 1; LE p1,p1,P,p1,p2 by A1,A2,JORDAN5C:9; then x in {q: LE q,p1,P,p1,p2} by A4; hence x in L_Segment(P,p1,p2,p1) by Def3; end; canceled 2; theorem for P being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds L_Segment(P,p1,p2,p2)=P proof let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; assume A1:P is_an_arc_of p1,p2; thus L_Segment(P,p1,p2,p2) c= P by Th20; let x;assume A2:x in P; then reconsider p=x as Point of TOP-REAL 2; LE p,p2,P,p1,p2 by A1,A2,JORDAN5C:10; then x in {q: LE q,p2,P,p1,p2}; hence x in L_Segment(P,p1,p2,p2) by Def3; end; theorem for P being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds R_Segment(P,p1,p2,p2)={p2} proof let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; assume A1: P is_an_arc_of p1,p2; then A2:p2 in P by TOPREAL1:4; thus R_Segment(P,p1,p2,p2) c= {p2} proof let x;assume x in R_Segment(P,p1,p2,p2); then x in {q: LE p2,q,P,p1,p2} by Def4; then consider q such that A3:q=x & LE p2,q,P,p1,p2; q in P by A3,JORDAN5C:def 3; then LE p1,q,P,p1,p2 & LE q,p2,P,p1,p2 by A1,JORDAN5C:10; then q=p2 by A1,A3,JORDAN5C:12; hence x in {p2} by A3,TARSKI:def 1; end; let x;assume x in {p2}; then A4:x=p2 by TARSKI:def 1; LE p2,p2,P,p1,p2 by A1,A2,JORDAN5C:9; then x in {q: LE p2,q,P,p1,p2} by A4; hence x in R_Segment(P,p1,p2,p2) by Def4; end; theorem for P being Subset of TOP-REAL 2,p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds R_Segment(P,p1,p2,p1)=P proof let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; assume A1:P is_an_arc_of p1,p2; thus R_Segment(P,p1,p2,p1) c= P by Th21; let x;assume A2:x in P; then reconsider p=x as Point of TOP-REAL 2; LE p1,p,P,p1,p2 by A1,A2,JORDAN5C:10; then x in {q: LE p1,q,P,p1,p2}; hence x in R_Segment(P,p1,p2,p1) by Def4; end; theorem for P being Subset of TOP-REAL 2, p1,p2,q1 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & q1 in P holds R_Segment(P,p1,p2,q1)=L_Segment(P,p2,p1,q1) proof let P be Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2; assume A1: P is_an_arc_of p1,p2 & q1 in P; then A2:P is_an_arc_of p2,p1 by JORDAN5B:14; A3:R_Segment(P,p1,p2,q1)= {q: LE q1,q,P,p1,p2} by Def4; A4:L_Segment(P,p2,p1,q1)= {q : LE q,q1,P,p2,p1} by Def3; A5: {q: LE q1,q,P,p1,p2} c= {q2 : LE q2,q1,P,p2,p1} proof let x;assume x in {q: LE q1,q,P,p1,p2}; then consider q such that A6:q=x & LE q1,q,P,p1,p2; LE q,q1,P,p2,p1 by A1,A6,Th19; hence x in {q2 : LE q2,q1,P,p2,p1} by A6; end; {q2 : LE q2,q1,P,p2,p1} c= {q: LE q1,q,P,p1,p2} proof let x;assume x in {q: LE q,q1,P,p2,p1}; then consider q such that A7:q=x & LE q,q1,P,p2,p1; LE q1,q,P,p1,p2 by A2,A7,Th19; hence x in {q2 : LE q1,q2,P,p1,p2} by A7; end; hence thesis by A3,A4,A5,XBOOLE_0:def 10; end; definition let P be Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2; func Segment(P,p1,p2,q1,q2) -> Subset of TOP-REAL 2 equals :Def5: R_Segment(P,p1,p2,q1) /\ L_Segment(P,p1,p2,q2); correctness; end; theorem for P being Subset of TOP-REAL 2, p1,p2,q1,q2 being Point of TOP-REAL 2 holds Segment(P,p1,p2,q1,q2)={q:LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2} proof let P be Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2; thus Segment(P,p1,p2,q1,q2) c= {q:LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2} proof let x;assume x in Segment(P,p1,p2,q1,q2); then x in R_Segment(P,p1,p2,q1) /\ L_Segment(P,p1,p2,q2) by Def5; then A1:x in R_Segment(P,p1,p2,q1) & x in L_Segment(P,p1,p2,q2) by XBOOLE_0:def 3; then x in {q: LE q1,q,P,p1,p2} by Def4; then consider q such that A2:q=x & (LE q1,q,P,p1,p2); x in {p: LE p,q2,P,p1,p2} by A1,Def3; then consider p such that A3: p=x & (LE p,q2,P,p1,p2); thus x in {p3:LE q1,p3,P,p1,p2 & LE p3,q2,P,p1,p2} by A2,A3; end; let x;assume x in {q:LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2}; then consider q such that A4: q=x & (LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2) ; x in {q3: LE q1,q3,P,p1,p2} by A4; then A5:x in R_Segment(P,p1,p2,q1) by Def4; x in {q3: LE q3,q2,P,p1,p2} by A4; then x in L_Segment(P,p1,p2,q2) by Def3; then x in R_Segment(P,p1,p2,q1) /\ L_Segment(P,p1,p2,q2) by A5,XBOOLE_0 :def 3; hence x in Segment(P,p1,p2,q1,q2) by Def5; end; theorem Th30: for P being Subset of TOP-REAL 2, p1,p2,q1,q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds LE q1,q2,P,p1,p2 iff LE q2,q1,P,p2,p1 proof let P be Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2; assume A1: P is_an_arc_of p1,p2; then P is_an_arc_of p2,p1 by JORDAN5B:14; hence thesis by A1,Th19; end; theorem Th31: for P being Subset of TOP-REAL 2, p1,p2,q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & q in P holds L_Segment(P,p1,p2,q)=R_Segment(P,p2,p1,q) proof let P be Subset of TOP-REAL 2, p1,p2,q be Point of TOP-REAL 2; assume A1:P is_an_arc_of p1,p2 & q in P; thus L_Segment(P,p1,p2,q) c= R_Segment(P,p2,p1,q) proof let x;assume x in L_Segment(P,p1,p2,q); then x in {p: LE p,q,P,p1,p2} by Def3; then consider p such that A2: p=x & (LE p,q,P,p1,p2); LE q,p,P,p2,p1 by A1,A2,Th30; then x in {q1: LE q,q1,P,p2,p1} by A2; hence x in R_Segment(P,p2,p1,q) by Def4; end; let x;assume x in R_Segment(P,p2,p1,q); then x in {p: LE q,p,P,p2,p1} by Def4; then consider p such that A3: p=x & (LE q,p,P,p2,p1); LE p,q,P,p1,p2 by A1,A3,Th30; then x in {q1: LE q1,q,P,p1,p2} by A3; hence x in L_Segment(P,p1,p2,q) by Def3; end; theorem for P being Subset of TOP-REAL 2, p1,p2,q1,q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & q1 in P & q2 in P holds Segment(P,p1,p2,q1,q2)=Segment(P,p2,p1,q2,q1) proof let P be Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2; assume A1:P is_an_arc_of p1,p2 & q1 in P & q2 in P; A2:Segment(P,p1,p2,q1,q2)=R_Segment(P,p1,p2,q1)/\ L_Segment(P,p1,p2,q2) by Def5; A3:L_Segment(P,p1,p2,q2)=R_Segment(P,p2,p1,q2) by A1,Th31; P is_an_arc_of p2,p1 by A1,JORDAN5B:14; then R_Segment(P,p1,p2,q1)=L_Segment(P,p2,p1,q1) by A1,Th31; hence thesis by A2,A3,Def5; end; begin ::Decomposition of a Simple Closed Curve into Two Arcs definition let s be real number; func Vertical_Line(s) -> Subset of TOP-REAL 2 equals :Def6: {p where p is Point of TOP-REAL 2: p`1=s}; correctness proof {p where p is Point of TOP-REAL 2: p`1=s} c= the carrier of (TOP-REAL 2) proof let x;assume x in {p where p is Point of TOP-REAL 2: p`1=s}; then ex p being Point of TOP-REAL 2 st p=x & p`1=s; hence x in the carrier of (TOP-REAL 2); end; hence thesis; end; func Horizontal_Line(s) -> Subset of TOP-REAL 2 equals :Def7: {p: p`2=s}; correctness proof {p where p is Point of TOP-REAL 2: p`2=s} c= the carrier of (TOP-REAL 2) proof let x;assume x in {p where p is Point of TOP-REAL 2: p`2=s}; then ex p being Point of TOP-REAL 2 st p=x & p`2=s; hence x in the carrier of (TOP-REAL 2); end; hence thesis; end; end; theorem Th33:for r being real number holds Vertical_Line(r) is closed & Horizontal_Line(r) is closed proof let r be real number; A1: Vertical_Line(r)={p where p is Point of TOP-REAL 2: p`1=r} by Def6; Horizontal_Line(r)={p where p is Point of TOP-REAL 2: p`2=r} by Def7; hence thesis by A1,Th7,Th10; end; theorem Th34: for r being real number,p being Point of TOP-REAL 2 holds p in Vertical_Line(r) iff p`1=r proof let r be real number,p be Point of TOP-REAL 2; hereby assume p in Vertical_Line(r); then p in {q where q is Point of TOP-REAL 2: q`1=r} by Def6; then ex q being Point of TOP-REAL 2 st q=p & q`1=r; hence p`1=r; end; assume p`1 = r; then p in {p1 where p1 is Point of TOP-REAL 2: p1`1=r}; hence thesis by Def6; end; theorem for r being real number,p being Point of TOP-REAL 2 holds p in Horizontal_Line(r) iff p`2=r proof let r be real number,p be Point of TOP-REAL 2; hereby assume p in Horizontal_Line(r); then p in {q where q is Point of TOP-REAL 2: q`2=r} by Def7; then ex q being Point of TOP-REAL 2 st q=p & q`2=r; hence p`2=r; end; assume p`2 = r; then p in {p1 where p1 is Point of TOP-REAL 2: p1`2=r}; hence thesis by Def7; end; canceled 4; theorem Th40: for P being compact non empty Subset of TOP-REAL 2 st P is_simple_closed_curve ex P1,P2 being non empty Subset of TOP-REAL 2 st P1 is_an_arc_of W-min(P),E-max(P) & P2 is_an_arc_of E-max(P),W-min(P) & P1 /\ P2={W-min(P),E-max(P)} & P1 \/ P2=P & First_Point(P1,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2 proof let P be compact non empty Subset of TOP-REAL 2; assume A1:P is_simple_closed_curve; A2:W-min(P) in P & E-max(P) in P by SPRECT_1:15,16; W-min(P)<>E-max(P) by A1,TOPREAL5:25; then consider P01,P02 being non empty Subset of TOP-REAL 2 such that A3:P01 is_an_arc_of W-min(P),E-max(P) & P02 is_an_arc_of W-min(P),E-max(P) & P = P01 \/ P02 & P01 /\ P02 = {W-min(P),E-max(P)} by A1,A2,TOPREAL2:5; reconsider P01,P02 as non empty Subset of TOP-REAL 2; A4:P01 is_an_arc_of E-max(P),W-min(P) by A3,JORDAN5B:14; A5:P02 is_an_arc_of E-max(P),W-min(P) by A3,JORDAN5B:14; reconsider P001=P01, P002=P02 as non empty Subset of TOP-REAL 2; A6:(E-max P)`1 = E-bound P by PSCOMP_1:104; A7:Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by Th33; P01 is closed by A3,Th12; then A8:P01/\Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by A7,TOPS_1:35; A9:Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by Th33; P02 is closed by A3,Th12; then A10:P02/\Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by A9,TOPS_1:35; consider q1 being Point of TOP-REAL 2 such that A11: q1 in P001 & q1`1 = ((W-min(P))`1+(E-max(P))`1)/2 by A3,Th13; A12:(W-min P)`1 = W-bound P by PSCOMP_1:84; (E-max P)`1 = E-bound P by PSCOMP_1:104; then q1 in {p where p is Point of TOP-REAL 2: p`1=(W-bound(P)+E-bound(P ))/2} by A11,A12; then q1 in Vertical_Line((W-bound(P)+E-bound(P))/2) by Def6; then P01/\Vertical_Line((W-bound(P)+E-bound(P))/2) <> {} by A11,XBOOLE_0:def 3; then A13:P01 meets Vertical_Line((W-bound(P)+E-bound(P))/2) by XBOOLE_0: def 7; consider q2 being Point of TOP-REAL 2 such that A14: q2 in P002 & q2`1 = ((W-min(P))`1+(E-max(P))`1)/2 by A3,Th13; q2 in {p where p is Point of TOP-REAL 2: p`1=(W-bound(P)+E-bound(P))/2 } by A6,A12,A14; then q2 in Vertical_Line((W-bound(P)+E-bound(P))/2) by Def6; then P02/\Vertical_Line((W-bound(P)+E-bound(P))/2) <> {} by A14,XBOOLE_0:def 3; then A15:P02 meets Vertical_Line((W-bound(P)+E-bound(P))/2) by XBOOLE_0: def 7 ; per cases; suppose First_Point(P01,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P02,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2; hence thesis by A3,A5; suppose A16:First_Point(P01,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2<= Last_Point(P02,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2; now per cases by A16,REAL_1:def 5; case A17:First_Point(P01,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2< Last_Point(P02,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2; A18:First_Point(P01,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2)) = Last_Point(P01,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2)) by A3,A8,A13,JORDAN5C:18; Last_Point(P02,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2)) = First_Point(P02,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2)) by A3,A10,A15,JORDAN5C:18; hence ex P1,P2 being non empty Subset of TOP-REAL 2 st P1 is_an_arc_of W-min(P),E-max(P) & P2 is_an_arc_of E-max(P),W-min(P) & P1 /\ P2={W-min(P),E-max(P)} & P1 \/ P2=P & First_Point(P1,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by A3,A4,A17,A18; case A19:First_Point(P01,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2= Last_Point(P02,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2; set p=First_Point(P01,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2)); set p'=Last_Point(P02,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2)); A20:W-bound(P)<E-bound(P) by A1,TOPREAL5:23; A21:p in P01/\ Vertical_Line((W-bound(P)+E-bound(P))/2) by A3,A8,A13,JORDAN5C:def 1; then A22:p in P01 by XBOOLE_0:def 3; p in Vertical_Line((W-bound(P)+E-bound(P))/2) by A21,XBOOLE_0:def 3 ; then A23:p`1=(W-bound(P)+E-bound(P))/2 by Th34; A24:p' in P02/\ Vertical_Line((W-bound(P)+E-bound(P))/2) by A5,A10,A15,JORDAN5C:def 2; then A25:p' in P02 by XBOOLE_0:def 3; p' in Vertical_Line((W-bound(P)+E-bound(P))/2) by A24,XBOOLE_0:def 3 ; then p'`1=(W-bound(P)+E-bound(P))/2 by Th34; then p=p' by A19,A23,TOPREAL3:11; then p in P01 /\ P02 by A22,A25,XBOOLE_0:def 3; then p=W-min(P) or p=E-max(P) by A3,TARSKI:def 2; hence contradiction by A6,A12,A20,A23,XCMPLX_1:67; end; then consider P1,P2 being non empty Subset of TOP-REAL 2 such that A26: P1 is_an_arc_of W-min(P),E-max(P) & P2 is_an_arc_of E-max(P),W-min(P) & P1 /\ P2={W-min(P),E-max(P)} & P1 \/ P2=P & First_Point(P1,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2; reconsider P1,P2 as non empty Subset of TOP-REAL 2; take P1, P2; thus thesis by A26; end; begin ::Uniqueness of Decomposition of a Simple Closed Curve theorem Th41:for P being Subset of I[01] st P=(the carrier of I[01]) \{0,1} holds P is open proof let P be Subset of I[01]; assume A1:P=(the carrier of I[01]) \{0,1}; A2:0 in [.0,1.] by TOPREAL5:1; A3:1 in [.0,1.] by TOPREAL5:1; {0} is Subset of I[01] by A2,BORSUK_1:83,ZFMISC_1:37; then reconsider Q0={0} as Subset of I[01]; A4:Q0 is closed by A2,BORSUK_1:83,PCOMPS_1:10; {1} is Subset of I[01] by A3,BORSUK_1:83,ZFMISC_1:37; then reconsider Q1={1} as Subset of I[01]; Q1 is closed by A3,BORSUK_1:83,PCOMPS_1:10; then A5:Q0 \/ Q1 is closed by A4,TOPS_1:36; A6:Q0 \/ Q1={0,1} by ENUMSET1:41; [#](I[01])\(Q0 \/ Q1) is open by A5,PRE_TOPC:def 6; hence P is open by A1,A6,PRE_TOPC:12; end; canceled 2; theorem Th44:for r,s being real number holds ].r,s.[ misses {r,s} proof let r,s be real number; assume A1: ].r,s.[ /\{r,s}<>{}; consider x being Element of ].r,s.[ /\ {r,s}; A2:x in ].r,s.[ & x in {r,s} by A1,XBOOLE_0:def 3; then reconsider r1=x as Real; r1 in {s1 where s1 is Real :r<s1 & s1<s} by A2,RCOMP_1:def 2; then consider s1 being Real such that A3:s1=r1 & (r<s1 & s1<s); thus contradiction by A2,A3,TARSKI:def 2; end; theorem Th45: for a,b,c being real number holds c in ].a,b.[ iff a < c & c < b proof let a,b,c be real number; A1: c is Real by XREAL_0:def 1; A2:now assume c in ].a,b.[; then c in {r where r is Real:a<r & r<b} by RCOMP_1:def 2; then consider r being Real such that A3: r=c & (a<r & r<b); thus a<c & c <b by A3; end; now assume a < c & c < b; then c in {r where r is Real:a<r & r<b} by A1; hence c in ].a,b.[ by RCOMP_1:def 2; end; hence thesis by A2; end; theorem for P being Subset of R^1, r,s being real number st P=].r,s.[ holds P is open proof let P be Subset of R^1, r,s be real number; assume A1: P=].r,s.[; {r1:r<r1} c= REAL proof let x;assume x in {r1:r<r1}; then consider r1 such that A2:r1=x & r<r1; thus x in REAL by A2; end; then reconsider P1={r1 where r1 is Real:r<r1} as Subset of R^1 by TOPMETR:24; {r2:s>r2} c= REAL proof let x;assume x in {r2:s>r2}; then consider r2 such that A3:r2=x & s>r2; thus x in REAL by A3; end; then reconsider P2={r2 where r2 is Real:s>r2} as Subset of R^1 by TOPMETR:24; A4:P1 is open by TOPREAL5:7; A5:P2 is open by TOPREAL5:8; P=P1 /\ P2 proof A6:P c= P1 /\ P2 proof let x;assume A7:x in P; then reconsider r1=x as Real by TOPMETR:24; A8:r<r1 & r1<s by A1,A7,Th45; then A9:x in P1; x in P2 by A8; hence x in P1 /\ P2 by A9,XBOOLE_0:def 3; end; P1 /\ P2 c= P proof let x;assume x in P1 /\ P2; then A10:x in P1 & x in P2 by XBOOLE_0:def 3; then consider r1 such that A11:r1=x & r<r1; consider r2 such that A12:r2=x & s>r2 by A10; thus x in P by A1,A11,A12,Th45; end; hence thesis by A6,XBOOLE_0:def 10; end; hence P is open by A4,A5,TOPS_1:38; end; theorem Th47: for S being non empty TopSpace, P1,P2 being Subset of S, P1' being Subset of S|P2 st P1=P1' & P1 c= P2 holds S|P1=(S|P2)|P1' proof let S be non empty TopSpace, P1,P2 be Subset of S, P1' be Subset of S|P2; assume A1:P1=P1' & P1 c= P2; A2:[#](S|P2)=P2 by PRE_TOPC:def 10; [#](S|P2)=P2 by PRE_TOPC:def 10; then A3:the carrier of (S|P2)=P2 by PRE_TOPC:12; A4:[#]((S|P2)|P1')=P1 by A1,PRE_TOPC:def 10; P1 c= the carrier of S; then A5:[#]((S|P2)|P1') c= [#](S) by A4,PRE_TOPC:12; for R being Subset of (S|P2)|P1' holds R in the topology of (S|P2)|P1' iff ex Q being Subset of S st Q in the topology of S & R=Q/\[#]((S|P2)|P1') proof let R be Subset of (S|P2)|P1'; A6:now assume R in the topology of (S|P2)|P1'; then consider Q0 being Subset of S|P2 such that A7: Q0 in the topology of S|P2 & R=Q0/\[#]((S|P2)|P1') by PRE_TOPC:def 9; consider Q1 being Subset of S such that A8: Q1 in the topology of S & Q0=Q1/\[#](S|P2) by A7,PRE_TOPC:def 9; R=Q1/\(P2/\P1) by A2,A4,A7,A8,XBOOLE_1:16 .=Q1/\[#]((S|P2)|P1') by A1,A4,XBOOLE_1:28; hence ex Q being Subset of S st Q in the topology of S & R=Q/\[#]((S|P2)|P1') by A8; end; now given Q being Subset of S such that A9:Q in the topology of S & R=Q/\[#]((S|P2)|P1'); reconsider R'=Q/\[#](S|P2) as Subset of S|P2 by A2,A3,XBOOLE_1:17; A10:R' in the topology of (S|P2) by A9,PRE_TOPC:def 9; R'/\[#]((S|P2)|P1')=Q/\(P2/\P1) by A2,A4,XBOOLE_1:16 .=R by A1,A4,A9,XBOOLE_1:28; hence R in the topology of (S|P2)|P1' by A10,PRE_TOPC:def 9; end; hence R in the topology of (S|P2)|P1' iff ex Q being Subset of S st Q in the topology of S & R=Q/\[#]((S|P2)|P1') by A6; end; then (S|P2)|P1' is SubSpace of S by A5,PRE_TOPC:def 9; hence S|P1=(S|P2)|P1' by A4,PRE_TOPC:def 10; end; theorem Th48:for P7 being Subset of I[01] st P7=(the carrier of I[01]) \{0,1} holds P7<>{} & P7 is connected proof let P7 be Subset of I[01]; assume A1: P7=(the carrier of I[01]) \{0,1}; A2:1/2 in [.0,1.] by TOPREAL5:1; A3: not 1/2 in {0,1} by TARSKI:def 2; then A4:1/2 in [.0,1.]\{0,1} by A2,XBOOLE_0:def 4; A5:[#](I[01]|P7)=P7 by PRE_TOPC:def 10; then A6:the carrier of I[01]|P7=P7 by PRE_TOPC:12; for A,B being Subset of I[01]|P7 st [#](I[01]|P7) = A \/ B & A <> {}(I[01]|P7) & B <> {}(I[01]|P7) & A is open & B is open holds A meets B proof let A,B be Subset of I[01]|P7; assume that A7: [#](I[01]|P7) = A \/ B and A8: A <> {}(I[01]|P7) & B <> {}(I[01]|P7) and A9: A is open and A10: B is open; assume A11: A misses B; A12: ].0,1.[ misses {0,1} by Th44; A13:P7=(].0,1.[ \/ {0,1})\{0,1} by A1,BORSUK_1:83,RCOMP_1:11 .=].0,1.[ \{0,1} by XBOOLE_1:40 .=].0,1.[ by A12,XBOOLE_1:83; reconsider D1=[.0,1.] as Subset of R^1 by TOPMETR:24; reconsider P1=P7 as Subset of R^1 by A13,TOPMETR:24; I[01]=R^1|D1 by TOPMETR:26,27; then A14: I[01]|P7=R^1|P1 by Th47,BORSUK_1:83; P1={r1:0<r1 & r1<1} by A13,RCOMP_1:def 2; then P1 is open by JORDAN2B:32; then A15: I[01]|P7 is non empty open SubSpace of R^1 by A1,A4,A6,A14,BORSUK_1:83,STRUCT_0:def 1,TSEP_1:16; reconsider P = A, Q = B as non empty Subset of REAL by A6,A8,A13,XBOOLE_1:1; the carrier of RealSpace = the carrier of TopSpaceMetr(RealSpace) by TOPMETR:16; then reconsider A0 = P, B0 = Q as non empty Subset of R^1 by METRIC_1:def 14,TOPMETR:def 7; A16: A0 is open & B0 is open by A9,A10,A15,TSEP_1:17; consider xp being Element of P; reconsider xp as Real; A17: xp in P; A18: P is bounded_below proof now take p = 0; let r be real number; assume r in P; then r in ].0,1.[ by A6,A13; then r in {w where w is Real : 0<w & w<1} by RCOMP_1:def 2; then ex u being Real st u = r & 0<u & u<1; hence p <= r; end; hence thesis by SEQ_4:def 2; end; A19: Q is bounded_below proof now take p = 0; let r be real number; assume r in Q; then r in ].0,1.[ by A6,A13; then r in {w where w is Real : 0<w & w<1} by RCOMP_1:def 2; then ex u being Real st u = r & 0<u & u<1; hence p <= r; end; hence thesis by SEQ_4:def 2; end; reconsider l = lower_bound Q as Element of REAL by XREAL_0:def 1; reconsider m = l as Point of RealSpace by METRIC_1:def 14; reconsider t = m as Point of R^1 by TOPMETR:16,def 7; A20: not l in Q proof assume l in Q; then consider s being real number such that A21: s > 0 and A22: Ball(m,s) c= B0 by A16,TOPMETR:22,def 7; reconsider s as Element of REAL by XREAL_0:def 1; reconsider e1 = l-s/2 as Point of RealSpace by METRIC_1:def 14; A23:l-(l-s/2)=s/2 by XCMPLX_1:18; A24:s/2>0 by A21,REAL_2:127; s/2<s by A21,SEQ_2:4; then abs(l - (l-s/2)) < s by A23,A24,ABSVALUE:def 1; then (the distance of RealSpace).(m,e1) < s by METRIC_1:def 13,def 14; then dist(m,e1) < s by METRIC_1:def 1; then e1 in {z where z is Element of RealSpace : dist(m,z)<s}; then l-s/2 in Ball(m,s) by METRIC_1:18; then l<=l-s/2 by A19,A22,SEQ_4:def 5; then l+s/2<=l by REAL_1: 84; then l+s/2-l<=l-l by REAL_1:49; then s/2<=l-l by XCMPLX_1:26; then s/2<=0 by XCMPLX_1:14; hence contradiction by A21,REAL_2:127; end; A25: now assume A26:l<=0; 0<xp & xp<1 by A6,A13,A17,Th45; then xp-l>0 by A26,SQUARE_1:11; then consider r5 being real number such that A27: (r5 in Q & r5<l+(xp-l)) by A19,SEQ_4:def 5; reconsider r5 as Real by XREAL_0:def 1; A28:r5<xp by A27,XCMPLX_1:27; A29:{s5 where s5 is Real:s5 in P & r5<s5} c= P proof let y be set; assume y in {s5 where s5 is Real:s5 in P & r5<s5}; then ex s5 being Real st s5=y & s5 in P & r5<s5; hence y in P; end; then reconsider P5={s5 where s5 is Real:s5 in P & r5<s5} as Subset of REAL by XBOOLE_1:1; A30:xp in P5 by A28; A31: P5 is bounded_below by A18,A29,RCOMP_1:3; reconsider l5 = lower_bound P5 as Real by XREAL_0:def 1; reconsider m5 = l5 as Point of RealSpace by METRIC_1:def 14; A32: now assume A33:l5<=r5; now assume l5<r5; then r5-l5>0 by SQUARE_1:11; then consider r be real number such that A34: r in P5 & r<l5+(r5-l5) by A30,A31,SEQ_4:def 5; consider s6 being Real such that A35:s6=r & s6 in P & r5<s6 by A34; thus contradiction by A34,A35,XCMPLX_1:27; end; then l5=r5 by A33,AXIOMS:21; then consider r7 being real number such that A36: r7 > 0 and A37: Ball(m5,r7) c= B0 by A16,A27,TOPMETR:22,def 7; consider r9 being real number such that A38: r9 in P5 & r9<l5+r7 by A30,A31,A36,SEQ_4:def 5; reconsider r9 as Real by XREAL_0:def 1; reconsider e8=r9 as Point of RealSpace by METRIC_1:def 14; l5<=r9 by A31,A38,SEQ_4:def 5; then A39:r9-l5>=0 by SQUARE_1:12; r9-l5<l5+r7-l5 by A38,REAL_1:54; then r9-l5<r7 by XCMPLX_1:26; then abs(r9 - l5) < r7 by A39,ABSVALUE:def 1; then (the distance of RealSpace).(e8,m5) < r7 by METRIC_1:def 13,def 14; then dist(e8,m5) < r7 by METRIC_1:def 1; then e8 in {z where z is Element of RealSpace : dist(m5,z)<r7}; then e8 in Ball(m5,r7) by METRIC_1:18; hence contradiction by A11,A29,A37,A38,XBOOLE_0:3; end; 0<r5 & r5<1 by A6,A13,A27,Th45; then A40:l5>0 by A32,AXIOMS:22; A41:l5-r5>0 by A32,SQUARE_1:11; consider q being Element of P5; A42:q in P5 by A30; then reconsider q1=q as Real; q1 in P by A29,A42; then A43:0<q1 & q1<1 by A6,A13,Th45; l5<=q1 by A30,A31,SEQ_4:def 5; then l5<1 by A43,AXIOMS:22; then l5 in ].0,1.[ by A40,Th45; then A44:l5 in P or l5 in Q by A5,A7,A13,XBOOLE_0:def 2; now assume l5 in P; then consider s5 being real number such that A45: s5 > 0 and A46: Ball(m5,s5) c= P by A16,TOPMETR:22,def 7; reconsider s5 as Element of REAL by XREAL_0:def 1; set s5'=min(s5,l5-r5); A47:s5'>0 by A41,A45,SPPOL_1:13; then A48:s5'/2>0 by REAL_2:127; A49:s5'<=s5 by SQUARE_1:35; A50:s5'/2<s5' by A47,SEQ_2:4; s5'<=l5-r5 by SQUARE_1:35; then s5'/2<l5-r5 by A50,AXIOMS:22; then s5'/2+r5<l5-r5+r5 by REAL_1:53; then s5'/2+r5<l5 by XCMPLX_1:27; then s5'/2+r5-s5'/2<l5-s5'/2 by REAL_1:54; then A51:r5<l5-s5'/2 by XCMPLX_1:26; reconsider e1 = l5-s5'/2 as Point of RealSpace by METRIC_1:def 14; A52:l5-(l5-s5'/2)=s5'/2 by XCMPLX_1:18; s5'/2<s5' by A47,SEQ_2:4; then s5'/2<s5 by A49,AXIOMS:22; then abs(l5 - (l5-s5'/2)) < s5 by A48,A52,ABSVALUE:def 1; then (real_dist).(l5,l5-s5'/2) < s5 by METRIC_1:def 13; then dist(m5,e1) < s5 by METRIC_1:def 1,def 14; then e1 in {z where z is Element of RealSpace : dist(m5,z)<s5}; then l5-s5'/2 in Ball(m5,s5) by METRIC_1:18; then l5-s5'/2 in {s7 where s7 is Real:s7 in P & r5<s7} by A46,A51; then A53:l5<=l5-s5'/2 by A31,SEQ_4:def 5; s5'/2>0 by A47,REAL_2:127; then l5<l5+s5'/2 by REAL_1:69; then l5-s5'/2<l5+s5'/2-s5'/2 by REAL_1:54; hence contradiction by A53,XCMPLX_1:26; end; then consider s1 being real number such that A54: s1 > 0 and A55: Ball(m5,s1) c= B0 by A16,A44,TOPMETR:22,def 7; s1/2>0 by A54,REAL_2:127; then consider r2 be real number such that A56:(r2 in P5 & r2<l5+s1/2) by A30,A31,SEQ_4:def 5; reconsider r2 as Real by XREAL_0:def 1; A57:l5<=r2 by A31,A56,SEQ_4:def 5; reconsider s3 = r2-l5 as Real; reconsider e1 = l5+s3 as Point of RealSpace by METRIC_1:def 14; A58:r2-l5>=0 by A57,SQUARE_1:12; A59:l5+s3-l5=s3 by XCMPLX_1:26; r2-l5<l5+s1/2-l5 by A56,REAL_1:92; then A60:s3<s1/2 by XCMPLX_1:26; s1/2<s1 by A54,SEQ_2:4; then A61:l5+s3-l5<s1 by A59,A60,AXIOMS:22; abs(l5+s3 - l5)=l5+s3-l5 by A58,A59,ABSVALUE:def 1; then (real_dist).(l5+s3,l5) < s1 by A61,METRIC_1:def 13; then dist(e1,m5) < s1 by METRIC_1:def 1,def 14; then l5+s3 in {z where z is Element of RealSpace : dist(m5,z)<s1}; then l5+s3 in Ball(m5,s1) & l5+s3 in P5 by A56,METRIC_1:18,XCMPLX_1:27; then A62:l5+s3 in P5 /\ Q by A55,XBOOLE_0:def 3; P5 /\ Q c= P /\ Q by A29,XBOOLE_1:26; hence contradiction by A11,A62,XBOOLE_0:def 7; end;consider q being Element of Q; A63:q in Q; reconsider q1=q as Real; A64:0<q1 & q1<1 by A6,A13,A63,Th45; l<=q1 by A19,SEQ_4:def 5; then l<1 by A64,AXIOMS:22; then l in ].0,1.[ by A25,Th45; then t in A0 & A0 is open by A5,A7,A9,A13,A15,A20,TSEP_1:17, XBOOLE_0:def 2; then consider s1 being real number such that A65: s1 > 0 and A66: Ball(m,s1) c= A0 by TOPMETR:22,def 7; s1/2>0 by A65,REAL_2:127; then consider r2 be real number such that A67: r2 in Q & r2<l+s1/2 by A19,SEQ_4:def 5; reconsider r2 as Real by XREAL_0:def 1; A68:l<=r2 by A19,A67,SEQ_4:def 5; set s3=r2-l; reconsider e1 = l+s3 as Point of RealSpace by METRIC_1:def 14; A69:r2-l>=0 by A68,SQUARE_1:12; A70:l+s3-l=s3 by XCMPLX_1:26; r2-l<l+s1/2-l by A67,REAL_1:92; then A71:s3<s1/2 by XCMPLX_1:26; s1/2<s1 by A65,SEQ_2:4; then A72:l+s3-l<s1 by A70,A71,AXIOMS:22; abs(l+s3 - l)=l+s3-l by A69,A70,ABSVALUE:def 1; then (real_dist).(l+s3,l) < s1 by A72,METRIC_1:def 13; then dist(e1,m) < s1 by METRIC_1:def 1,def 14; then l+s3 in {z where z is Element of RealSpace : dist(m,z)<s1}; then l+s3 in Ball(m,s1) & l+s3 in Q by A67,METRIC_1:18,XCMPLX_1:27 ; hence contradiction by A11,A66,XBOOLE_0:3; end; then I[01]|P7 is connected by CONNSP_1:12; hence thesis by A1,A2,A3,BORSUK_1:83,CONNSP_1:def 3,XBOOLE_0:def 4; end; theorem Th49:for P being Subset of TOP-REAL n, p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 holds p1<>p2 proof let P be Subset of TOP-REAL n, p1,p2 be Point of TOP-REAL n; assume P is_an_arc_of p1,p2; then consider f being map of I[01], (TOP-REAL n)|P such that A1:f is_homeomorphism & f.0 = p1 & f.1 = p2 by TOPREAL1:def 2; 1 in [.0,1.] by TOPREAL5:1; then 1 in [#](I[01]) by BORSUK_1:83,PRE_TOPC:12; then A2:1 in dom f by A1,TOPS_2:def 5; A3:f is one-to-one by A1,TOPS_2:def 5; 0 in [.0,1.] by TOPREAL5:1; then 0 in [#](I[01]) by BORSUK_1:83,PRE_TOPC:12; then 0 in dom f by A1,TOPS_2:def 5; hence thesis by A1,A2,A3,FUNCT_1:def 8; end; theorem for P being Subset of TOP-REAL n, Q being Subset of (TOP-REAL n)|P, p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 & Q=P\{p1,p2} holds Q is open proof let P be Subset of TOP-REAL n, Q be Subset of (TOP-REAL n)|P, p1,p2 be Point of TOP-REAL n; assume A1:P is_an_arc_of p1,p2 & Q=P\{p1,p2}; then reconsider P' = P as non empty Subset of TOP-REAL n by TOPREAL1:4; consider f being map of I[01], (TOP-REAL n)|P' such that A2:f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2; reconsider f1=f as Function; A3:f" is_homeomorphism by A2,TOPS_2:70; reconsider g=f" as map of (TOP-REAL n)|P,I[01]; reconsider g1=g as Function; (the carrier of I[01])\{0,1} is Subset of I[01] by XBOOLE_1: 36 ; then reconsider R=(the carrier of I[01])\{0,1} as Subset of I[01]; A4:R is open by Th41; A5:f is one-to-one by A2,TOPS_2:def 5; A6:g is one-to-one by A3,TOPS_2:def 5; A7:g is continuous by A2,TOPS_2:def 5; A8:[#](I[01])=dom f by A2,TOPS_2:def 5; 0 in [.0,1.] by TOPREAL5:1; then 0 in [#](I[01]) by BORSUK_1:83,PRE_TOPC:12; then A9:0 in dom f by A2,TOPS_2:def 5; 1 in the carrier of I[01] by BORSUK_1:83,TOPREAL5:1; then 1 in [#](I[01]) by PRE_TOPC:12; then A10:1 in dom f by A2,TOPS_2:def 5; rng f=[#]((TOP-REAL n)|P) by A2,TOPS_2:def 5; then A11:f""=f by A5,TOPS_2:64; rng g= [#](I[01]) by A3,TOPS_2:def 5; then A12: g1" =f1 by A6,A11,TOPS_2:def 4; g"(R)=g1"(the carrier of I[01])\g1"({0,1}) by FUNCT_1:138 .=((g1").:(the carrier of I[01]))\g1"({0,1}) by A6,FUNCT_1:155 .=f1.:(the carrier of I[01])\ (g1").:({0,1}) by A6,A12,FUNCT_1:155 .=f1.:([#](I[01]))\ f1.:({0,1}) by A12,PRE_TOPC:12 .=rng f\ f.:({0,1}) by A8,RELAT_1:146 .=[#]((TOP-REAL n)|P)\ f.:({0,1}) by A2,TOPS_2:def 5 .=P\ f.:({0,1}) by PRE_TOPC:def 10 .=Q by A1,A2,A9,A10,FUNCT_1:118; hence thesis by A4,A7,TOPS_2:55; end; ::A proof of the following is almost same as JORDAN5A:1. canceled; theorem Th52: for P being Subset of TOP-REAL n, P1,P2 being non empty Subset of TOP-REAL n, Q being Subset of (TOP-REAL n)|P, p1,p2 being Point of TOP-REAL n st p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2={p1,p2} & Q=P1\{p1,p2} holds Q is open proof let P be Subset of TOP-REAL n, P1,P2 be non empty Subset of TOP-REAL n, Q be Subset of (TOP-REAL n)|P, p1,p2 be Point of TOP-REAL n; assume A1: p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2={p1,p2} & Q=P1\{p1,p2}; reconsider P21=P2 as Subset of TOP-REAL n; A2: P21 is compact by A1,JORDAN5A:1; p1 in P1 /\ P2 by A1,TARSKI:def 2; then A3:p1 in P1 & p1 in P2 by XBOOLE_0:def 3; A4:[#]((TOP-REAL n)|P)=P by PRE_TOPC:def 10; then A5:the carrier of (TOP-REAL n)|P=P by PRE_TOPC:12; A6:(TOP-REAL n)|P is non empty by A1,A4,STRUCT_0:def 1; P2 c= P by A1,XBOOLE_1:7; then reconsider P2'=P21 as Subset of (TOP-REAL n)|P by A5; p2 in P1 /\ P2 by A1,TARSKI:def 2; then A7:p2 in P1 & p2 in P2 by XBOOLE_0:def 3; A8:(TOP-REAL n)|P is_T2 by A6,TOPMETR:3; P21 c= [#]((TOP-REAL n)|P) by A1,A4,XBOOLE_1:7; then P2' is compact by A2,COMPTS_1:11; then A9:P2' is closed by A8,COMPTS_1:16; A10:P\P2= (P1 \P2) \/ (P2\P2) by A1,XBOOLE_1:42 .=(P1\P2) \/ {} by XBOOLE_1:37 .=P1\P2; P1\P2=Q proof A11:P1\P2 c= Q proof let x;assume x in P1\P2; then A12:x in P1 & not x in P2 by XBOOLE_0:def 4; then not x in {p1,p2} by A3,A7,TARSKI:def 2; hence x in Q by A1,A12,XBOOLE_0:def 4; end; Q c= P1\P2 proof let x;assume x in Q; then A13:x in P1 & not x in {p1,p2} by A1,XBOOLE_0:def 4; then not x in P2 by A1,XBOOLE_0:def 3; hence x in P1\P2 by A13,XBOOLE_0:def 4; end; hence thesis by A11,XBOOLE_0:def 10; end; then Q=P2'` by A5,A10,SUBSET_1:def 5; then Q= P2'`; hence thesis by A9,TOPS_1:29; end; theorem Th53: for P being Subset of TOP-REAL n, Q being Subset of (TOP-REAL n)|P, p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 & Q=P\{p1,p2} holds Q is connected proof let P be Subset of TOP-REAL n, Q be Subset of (TOP-REAL n)|P, p1,p2 be Point of TOP-REAL n; assume A1:P is_an_arc_of p1,p2 & Q=P\{p1,p2}; then reconsider P' = P as non empty Subset of TOP-REAL n by TOPREAL1:4; consider f being map of I[01], (TOP-REAL n)|P' such that A2: f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2; (the carrier of I[01]) \{0,1} is Subset of I[01] by XBOOLE_1:36; then reconsider P7=(the carrier of I[01]) \{0,1} as Subset of I[01]; A3:P7<>{} & P7 is connected by Th48; A4:f is continuous & f is one-to-one by A2,TOPS_2:def 5; Q=f.:P7 proof [#]((TOP-REAL n)|P)=P by PRE_TOPC:def 10; then A5:rng f=P by A2,TOPS_2:def 5; thus Q c= f.:P7 proof let x;assume x in Q; then A6:x in P & not x in {p1,p2} by A1,XBOOLE_0:def 4; then consider z being set such that A7: z in dom f & x=f.z by A5,FUNCT_1:def 5; A8: dom f=[#]I[01] by A2,TOPS_2:def 5; now assume z in {0,1}; then x=p1 or x=p2 by A2,A7,TARSKI:def 2; hence contradiction by A6,TARSKI:def 2; end; then z in P7 by A7,A8,XBOOLE_0:def 4; hence x in f.:P7 by A7,FUNCT_1:def 12; end; let y;assume y in f.:P7; then consider x such that A9:x in dom f & x in P7 & y=f.x by FUNCT_1:def 12; x in the carrier of I[01] & not x in {0,1} by A9,XBOOLE_0:def 4; then A10:x<>0 & x<>1 by TARSKI:def 2; A11:y in P by A5,A9,FUNCT_1:def 5; now assume A12: y in {p1,p2}; reconsider f1=f as Function of the carrier of I[01], the carrier of (TOP-REAL n)|P'; now per cases by A9,A12,TARSKI:def 2; case A13:f.x=p1; dom f1=the carrier of I[01] by FUNCT_2:def 1; then 0 in dom f1 by BORSUK_1:83,TOPREAL5:1; hence contradiction by A2,A4,A9,A10,A13,FUNCT_1:def 8; case A14:f.x=p2; dom f1=the carrier of I[01] by FUNCT_2:def 1; then 1 in dom f1 by BORSUK_1:83,TOPREAL5:1; hence contradiction by A2,A4,A9,A10,A14,FUNCT_1:def 8; end; hence contradiction; end; hence y in Q by A1,A11,XBOOLE_0:def 4; end; hence thesis by A3,A4,TOPREAL5:5; end; theorem Th54: for GX being non empty TopSpace, P1, P being Subset of GX, Q' being Subset of GX|P1, Q being Subset of GX|P st P1 c=P & Q=Q' & Q' is connected holds Q is connected proof let GX be non empty TopSpace, P1, P be Subset of GX, Q' be Subset of GX|P1, Q be Subset of GX|P; assume A1: P1 c=P & Q=Q' & Q' is connected; [#](GX|P)=P by PRE_TOPC:def 10; then P1 is Subset of GX|P by A1,PRE_TOPC:12; then reconsider P1'=P1 as Subset of GX|P; GX|P1=(GX|P)|P1' by A1,Th47; hence thesis by A1,CONNSP_3:34; end; theorem Th55: for P being Subset of TOP-REAL n, p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 ex p3 being Point of TOP-REAL n st p3 in P & p3<>p1 & p3<>p2 proof let P be Subset of TOP-REAL n, p1,p2 be Point of TOP-REAL n; assume P is_an_arc_of p1,p2; then consider f being map of I[01], (TOP-REAL n)|P such that A1:f is_homeomorphism & f.0 = p1 & f.1 = p2 by TOPREAL1:def 2; 1/2 in [.0,1.] by TOPREAL5:1; then 1/2 in [#](I[01]) by BORSUK_1:83,PRE_TOPC:12; then A2:1/2 in dom f by A1,TOPS_2:def 5; then f.(1/2) in rng f by FUNCT_1:def 5; then f.(1/2) in [#]((TOP-REAL n)|P) by A1,TOPS_2:def 5; then A3:f.(1/2) in P by PRE_TOPC:def 10; then reconsider p=f.(1/2) as Point of TOP-REAL n; A4:f is one-to-one by A1,TOPS_2:def 5; 0 in the carrier of I[01] by BORSUK_1:83,TOPREAL5:1; then 0 in [#](I[01]) by PRE_TOPC:12; then 0 in dom f by A1,TOPS_2:def 5; then A5:p1<>p by A1,A2,A4,FUNCT_1:def 8; 1 in [.0,1.] by TOPREAL5:1; then 1 in [#](I[01]) by BORSUK_1:83,PRE_TOPC:12; then 1 in dom f by A1,TOPS_2:def 5; then f.1<>f.(1/2) by A2,A4,FUNCT_1:def 8; hence thesis by A1,A3,A5; end; theorem for P being Subset of TOP-REAL n, p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 holds P\{p1,p2}<>{} proof let P be Subset of TOP-REAL n, p1,p2 be Point of TOP-REAL n; assume P is_an_arc_of p1,p2; then consider p3 being Point of TOP-REAL n such that A1: p3 in P & p3<>p1 & p3<>p2 by Th55; not p3 in {p1,p2} by A1,TARSKI:def 2; hence thesis by A1,XBOOLE_0:def 4; end; theorem for P1 being Subset of TOP-REAL n, P being Subset of TOP-REAL n, Q being Subset of (TOP-REAL n)|P, p1,p2 being Point of TOP-REAL n st P1 is_an_arc_of p1,p2 & P1 c=P & Q=P1\{p1,p2} holds Q is connected proof let P1 be Subset of TOP-REAL n, P be Subset of TOP-REAL n, Q be Subset of (TOP-REAL n)|P, p1,p2 be Point of TOP-REAL n; assume A1:P1 is_an_arc_of p1,p2 & P1 c=P & Q=P1\{p1,p2}; [#]((TOP-REAL n)|P1)=P1 by PRE_TOPC:def 10; then the carrier of (TOP-REAL n)|P1=P1 by PRE_TOPC:12; then Q is Subset of (TOP-REAL n)|P1 by A1,XBOOLE_1:36; then reconsider Q'=Q as Subset of (TOP-REAL n)|P1; Q' is connected by A1,Th53; hence thesis by A1,Th54; end; theorem Th58: for T,S,V being non empty TopSpace, P1 being non empty Subset of S, P2 being Subset of S, f being map of T,S|P1, g being map of S|P2,V st P1 c= P2 & f is continuous & g is continuous ex h being map of T,V st h=g*f & h is continuous proof let T,S,V be non empty TopSpace, P1 be non empty Subset of S, P2 be Subset of S, f be map of T,S|P1, g be map of S|P2,V; assume that A1: P1 c= P2 and A2: f is continuous and A3: g is continuous; reconsider P3 = P2 as non empty Subset of S by A1,XBOOLE_1:3; reconsider g1 = g as map of S|P3,V; [#](S|P1)=P1 by PRE_TOPC:def 10; then the carrier of (S|P1)=P1 by PRE_TOPC:12; then A4:f is Function of the carrier of T,P2 by A1,FUNCT_2:9; A5: [#](S|P2)=P2 by PRE_TOPC:def 10; then the carrier of (S|P2)=P2 by PRE_TOPC:12; then reconsider f1=f as map of T,S|P3 by A4; f1 is continuous proof for F1 being Subset of S|P2 st F1 is closed holds f1"F1 is closed proof let F1 be Subset of S|P2; assume A6:F1 is closed; reconsider P1'=P1 as non empty Subset of S|P3 by A1,A5, PRE_TOPC:12; [#](S|P1)=P1 by PRE_TOPC:def 10; then A7: the carrier of (S|P1)=P1 by PRE_TOPC:12; reconsider P4=F1/\P1' as Subset of (S|P3)|P1' by TOPS_2:38; A8:S|P1=(S|P3)|P1' by A1,Th47; A9: P4 is closed by A6,Th3; A10:f1"P1=the carrier of T by A7,FUNCT_2:48 .=dom f1 by FUNCT_2:def 1; f1"F1 c= dom f1 by RELAT_1:167; then f1"F1=f1"F1 /\ f1"P1 by A10,XBOOLE_1:28 .=f"P4 by FUNCT_1:137; hence f1"F1 is closed by A2,A8,A9,PRE_TOPC:def 12; end; hence f1 is continuous by PRE_TOPC:def 12; end; then g1*f1 is continuous by A3,TOPS_2:58; hence thesis; end; theorem Th59: for P1,P2 being Subset of TOP-REAL n, p1,p2 being Point of TOP-REAL n st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds P1=P2 proof let P1,P2 be Subset of TOP-REAL n, p1,p2 be Point of TOP-REAL n; assume A1:P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2; then reconsider P1' = P1, P2' = P2 as non empty Subset of TOP-REAL n by TOPREAL1:4; now assume A2:P2\P1<>{};consider p being Element of P2\P1; A3:p in P2 & not p in P1 by A2,XBOOLE_0:def 4; consider f1 being map of I[01],(TOP-REAL n)|P1' such that A4:f1 is_homeomorphism & f1.0=p1 & f1.1=p2 by A1,TOPREAL1:def 2; A5:f1 is continuous by A4,TOPS_2:def 5; consider f2 being map of I[01],(TOP-REAL n)|P2' such that A6:f2 is_homeomorphism & f2.0=p1 & f2.1=p2 by A1,TOPREAL1:def 2; reconsider f4=f2 as Function; A7:f2 is one-to-one by A6,TOPS_2:def 5; A8:dom f2=[#](I[01]) & rng f2=[#]((TOP-REAL n)|P2) by A6,TOPS_2:def 5; A9:f2" is_homeomorphism by A6,TOPS_2:70; then A10:dom (f2")=[#]((TOP-REAL n)|P2) by TOPS_2:def 5 .=P2 by PRE_TOPC:def 10; then A11:f2".p in rng (f2") by A3,FUNCT_1:def 5; f2" is continuous by A6,TOPS_2:def 5; then consider h being map of I[01],I[01] such that A12:h=f2"*f1 & h is continuous by A1,A5,Th58; h is Function of the carrier of Closed-Interval-TSpace(0,1), the carrier of R^1 by BORSUK_1:83,FUNCT_2:9,TOPMETR:24,27; then reconsider h1=h as map of Closed-Interval-TSpace(0,1),R^1 ; h1 is continuous proof for F1 being Subset of R^1 st F1 is closed holds h1"F1 is closed proof let F1 be Subset of R^1; assume A13:F1 is closed; reconsider K=the carrier of I[01] as Subset of R^1 by BORSUK_1:83,TOPMETR:24; A14:I[01]=R^1|K by BORSUK_1:83,TOPMETR:26,27; reconsider P3=F1/\K as Subset of R^1|K by TOPS_2:38; A15: P3 is closed by A13,Th3; A16:h1"K=the carrier of I[01] by FUNCT_2:48 .=dom h1 by FUNCT_2:def 1; h1"F1 c= dom h1 by RELAT_1:167; then h1"F1=h1"F1 /\ h1"K by A16,XBOOLE_1:28 .=h"P3 by FUNCT_1:137; hence h1"F1 is closed by A12,A14,A15,PRE_TOPC:def 12,TOPMETR:27; end; hence h1 is continuous by PRE_TOPC:def 12; end; then reconsider g=h1 as continuous map of Closed-Interval-TSpace(0,1),R^1; A17:dom f1 =[#](I[01]) by A4,TOPS_2:def 5 .=[.0,1.] by BORSUK_1:83,PRE_TOPC:12; then A18:0 in dom f1 by TOPREAL5:1; A19:1 in dom f1 by A17,TOPREAL5:1; A20:g.0=f2".p1 by A4,A12,A18,FUNCT_1:23; A21:g.1=f2".p2 by A4,A12,A19,FUNCT_1:23; A22:dom f2 =[#](I[01]) by A6,TOPS_2:def 5 .=[.0,1.] by BORSUK_1:83,PRE_TOPC:12; then A23:0 in dom f2 by TOPREAL5:1; A24:1 in dom f2 by A22,TOPREAL5:1; A25:(f2").p1=(f4").p1 by A7,A8,TOPS_2:def 4; ((f2)").p2=(f4").p2 by A7,A8,TOPS_2:def 4; then A26:g.0=0 & g.1=1 by A6,A7,A20,A21,A23,A24,A25,FUNCT_1:54; A27:f2".p in [.0,1.] by A11,BORSUK_1:83; A28:now assume f2".p in rng g; then consider x being set such that A29:x in dom g & f2".p=g.x by FUNCT_1:def 5; A30:f2".p=f2".(f1.x) by A12,A29,FUNCT_1:22; A31:x in dom f1 & f1.x in dom (f2") by A12,A29,FUNCT_1:21; f2" is one-to-one by A9,TOPS_2:def 5; then p=f1.x by A3,A10,A30,A31,FUNCT_1:def 8; then A32:p in rng f1 by A31,FUNCT_1:def 5; rng f1 =[#]((TOP-REAL n)|P1) by A4,TOPS_2:def 5 .=P1 by PRE_TOPC:def 10; hence contradiction by A2,A32,XBOOLE_0:def 4; end; reconsider r=f2".p as Real by A27; A33:rng f2=[#]((TOP-REAL n)|P2) by A6,TOPS_2:def 5 .=P2 by PRE_TOPC:def 10; A34:0<=r & r<=1 by A11,BORSUK_1:83,TOPREAL5:1; A35: now assume A36:r=0; f2.r=f4.((f4").p) by A7,A8,TOPS_2:def 4 .=p by A3,A7,A33,FUNCT_1:57; hence contradiction by A1,A3,A6,A36,TOPREAL1:4; end; now assume A37:r=1; f2.r= f4.((f4").p) by A7,A8,TOPS_2:def 4 .=p by A3,A7,A33,FUNCT_1:57; hence contradiction by A1,A3,A6,A37,TOPREAL1:4; end; then 0<r & r<1 by A34,A35,REAL_1:def 5; then consider rc being Real such that A38:g.rc=r & 0<rc & rc <1 by A26,TOPREAL5:12; the carrier of (TOP-REAL n)|P1 = [#]((TOP-REAL n)|P1) by PRE_TOPC:12 .=P1 by PRE_TOPC:def 10; then rng f1 c= dom (f2") by A1,A10,XBOOLE_1:1; then dom g=dom f1 by A12,RELAT_1:46 .=[#](I[01]) by A4,TOPS_2:def 5 .=[.0,1.] by BORSUK_1:83,PRE_TOPC:12; then rc in dom g by A38,TOPREAL5:1; hence contradiction by A28,A38,FUNCT_1:def 5; end; then P2 c= P1 by XBOOLE_1:37; hence P1=P2 by A1,XBOOLE_0:def 10; end; theorem Th60:for P being non empty Subset of TOP-REAL 2, Q being Subset of (TOP-REAL 2)|P, p1,p2 being Point of TOP-REAL 2 st P is_simple_closed_curve & p1 in P & p2 in P & p1<>p2 & Q=P\{p1,p2} holds not Q is connected proof let P be non empty Subset of TOP-REAL 2, Q be Subset of (TOP-REAL 2)|P, p1,p2 be Point of TOP-REAL 2; assume A1:P is_simple_closed_curve & p1 in P & p2 in P & p1<>p2 & Q=P\{p1,p2}; then consider P1,P2 being non empty Subset of TOP-REAL 2 such that A2: P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} by TOPREAL2:5; [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 10; then A3:the carrier of (TOP-REAL 2)|P=P by PRE_TOPC:12; A4:P1 c= P by A2,XBOOLE_1:7; P1\{p1,p2} c= P1 by XBOOLE_1:36; then P1\{p1,p2} is Subset of (TOP-REAL 2)|P by A3,A4,XBOOLE_1 :1; then reconsider P1'=P1\{p1,p2} as Subset of (TOP-REAL 2)|P; A5:P2 c= P by A2,XBOOLE_1:7; P2\{p1,p2} c= P2 by XBOOLE_1:36; then P2\{p1,p2} is Subset of (TOP-REAL 2)|P by A3,A5,XBOOLE_1 :1; then reconsider P2'=P2\{p1,p2} as Subset of (TOP-REAL 2)|P; A6:P1' is open by A1,A2,Th52; A7:P2' is open by A1,A2,Th52; A8:Q c= P1' \/ P2' proof let x;assume x in Q; then A9: x in P & not x in {p1,p2} by A1,XBOOLE_0:def 4; now per cases by A2,A9,XBOOLE_0:def 2; case (x in P1 & not x in {p1,p2}); then x in P1' by XBOOLE_0:def 4; hence x in P1' \/ P2' by XBOOLE_0:def 2; case (x in P2 & not x in {p1,p2}); then x in P2' by XBOOLE_0:def 4; hence x in P1' \/ P2' by XBOOLE_0:def 2; end; hence x in P1' \/ P2'; end; consider p3 being Point of TOP-REAL 2 such that A10:p3 in P1 & p3<>p1 & p3<>p2 by A2,Th55; not p3 in {p1,p2} by A10,TARSKI:def 2; then A11:P1'<>{} by A10,XBOOLE_0:def 4; P1' c= Q proof let x;assume x in P1'; then A12:x in P1 & not x in {p1,p2} by XBOOLE_0:def 4; then x in P by A2,XBOOLE_0:def 2; hence x in Q by A1,A12,XBOOLE_0:def 4; end; then (P1' /\ Q) <>{} by A11,XBOOLE_1:28; then A13:P1' meets Q by XBOOLE_0:def 7; consider p3' being Point of TOP-REAL 2 such that A14:p3' in P2 & p3'<>p1 & p3'<>p2 by A2,Th55; not p3' in {p1,p2} by A14,TARSKI:def 2; then A15:P2'<>{} by A14,XBOOLE_0:def 4; P2' c= Q proof let x;assume x in P2'; then A16:x in P2 & not x in {p1,p2} by XBOOLE_0:def 4; then x in P1 \/ P2 by XBOOLE_0:def 2; hence x in Q by A1,A2,A16,XBOOLE_0:def 4; end; then P2' /\ Q<>{} by A15,XBOOLE_1:28; then A17:P2' meets Q by XBOOLE_0:def 7; now assume P1' meets P2'; then consider p0 being set such that A18:p0 in P1' & p0 in P2' by XBOOLE_0:3; A19:p0 in P1 & not p0 in {p1,p2} by A18,XBOOLE_0:def 4; p0 in P2 by A18,XBOOLE_0:def 4; hence contradiction by A2,A19,XBOOLE_0:def 3; end; hence thesis by A6,A7,A8,A13,A17,TOPREAL5:4; end; theorem Th61: for P being non empty Subset of TOP-REAL 2, P1,P2,P1',P2' being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st P is_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2=P & P1' is_an_arc_of p1,p2 & P2' is_an_arc_of p1,p2 & P1' \/ P2'=P holds P1=P1' & P2=P2' or P1=P2' & P2=P1' proof let P be non empty Subset of TOP-REAL 2, P1,P2,P1',P2' be Subset of the carrier of TOP-REAL 2,p1,p2 be Point of TOP-REAL 2; assume that A1: P is_simple_closed_curve and A2: P1 is_an_arc_of p1,p2 and A3: P2 is_an_arc_of p1,p2 and A4: P1 \/ P2=P and A5: P1' is_an_arc_of p1,p2 and A6: P2' is_an_arc_of p1,p2 and A7: P1' \/ P2'=P; A8:p1<>p2 by A6,Th49; A9:P2' c= P by A7,XBOOLE_1:7; A10:p1 in P1' & p2 in P1' by A5,TOPREAL1:4; A11:P1' c= P by A7,XBOOLE_1:7; A12:p1 in P2 & p2 in P2 by A3,TOPREAL1:4; A13:p1 in P1 & p2 in P1 by A2,TOPREAL1:4; A14:P1 c= P by A4,XBOOLE_1:7; [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 10; then A15:the carrier of (TOP-REAL 2)|P=P by PRE_TOPC:12; P1\{p1,p2} c= P1 by XBOOLE_1:36; then P1\{p1,p2} is Subset of (TOP-REAL 2)|P by A14,A15,XBOOLE_1:1; then reconsider Q1=P1\{p1,p2} as Subset of (TOP-REAL 2)|P; A16:Q1 c= P1 by XBOOLE_1:36; A17:P2 c= P by A4,XBOOLE_1:7; P2\{p1,p2} c= P2 by XBOOLE_1:36; then P2\{p1,p2} is Subset of (TOP-REAL 2)|P by A15,A17,XBOOLE_1:1; then reconsider Q2=P2\{p1,p2} as Subset of (TOP-REAL 2)|P; A18:Q2 c= P2 by XBOOLE_1:36; A19:P1' c= P by A7,XBOOLE_1:7; P1'\{p1,p2} c= P1' by XBOOLE_1:36; then P1'\{p1,p2} is Subset of (TOP-REAL 2)|P by A15,A19,XBOOLE_1:1; then reconsider Q1'=P1'\{p1,p2} as Subset of (TOP-REAL 2)|P; A20:Q1' c= P1' by XBOOLE_1:36; A21:P2' c= P by A7,XBOOLE_1:7; P2'\{p1,p2} c= P2' by XBOOLE_1:36; then P2'\{p1,p2} is Subset of (TOP-REAL 2)|P by A15,A21,XBOOLE_1:1; then reconsider Q2'=P2'\{p1,p2} as Subset of (TOP-REAL 2)|P; A22:Q2' c= P2' by XBOOLE_1:36; A23:Q1 \/ Q2 =P\{p1,p2} by A4,XBOOLE_1:42; A24:Q1' \/ Q2' =P\{p1,p2} by A7,XBOOLE_1:42; then Q1' c=Q1 \/ Q2 by A23,XBOOLE_1:7; then A25:Q1' \/ (Q1 \/ Q2)=Q1 \/ Q2 by XBOOLE_1:12; Q2' c=Q1 \/ Q2 by A23,A24,XBOOLE_1:7; then A26:Q2' \/ (Q1 \/ Q2)=Q1 \/ Q2 by XBOOLE_1:12; Q1 c=Q1' \/ Q2' by A23,A24,XBOOLE_1:7; then A27:Q1 \/ (Q1' \/ Q2')=Q1' \/ Q2' by XBOOLE_1:12; Q2 c=Q1' \/ Q2' by A23,A24,XBOOLE_1:7; then A28:Q2 \/ (Q1' \/ Q2')=Q1' \/ Q2' by XBOOLE_1:12; [#]((TOP-REAL 2)|P1)=P1 by PRE_TOPC:def 10; then Q1 is Subset of (TOP-REAL 2)|P1 by A16,PRE_TOPC:12; then reconsider R1=Q1 as Subset of (TOP-REAL 2)|P1; R1 is connected by A2,Th53; then A29:Q1 is connected by A14,Th54; [#]((TOP-REAL 2)|P2)=P2 by PRE_TOPC:def 10; then Q2 is Subset of (TOP-REAL 2)|P2 by A18,PRE_TOPC:12; then reconsider R2=Q2 as Subset of (TOP-REAL 2)|P2; R2 is connected by A3,Th53; then A30:Q2 is connected by A17,Th54; [#]((TOP-REAL 2)|P1')=P1' by PRE_TOPC:def 10; then Q1' is Subset of (TOP-REAL 2)|P1' by A20,PRE_TOPC:12; then reconsider R1'=Q1' as Subset of (TOP-REAL 2)|P1'; R1' is connected by A5,Th53; then A31:Q1' is connected by A11,Th54; [#]((TOP-REAL 2)|P2')=P2' by PRE_TOPC:def 10; then Q2' is Subset of (TOP-REAL 2)|P2' by A22,PRE_TOPC:12; then reconsider R2'=Q2' as Subset of (TOP-REAL 2)|P2'; R2' is connected by A6,Th53; then A32:Q2' is connected by A9,Th54; A33: {p1,p2} c= P1 proof let x;assume x in {p1,p2}; hence x in P1 by A13,TARSKI:def 2; end; A34: {p1,p2} c= P2 proof let x;assume x in {p1,p2}; hence x in P2 by A12,TARSKI:def 2; end; A35: {p1,p2} c= P1' proof let x;assume x in {p1,p2}; hence x in P1' by A10,TARSKI:def 2; end; A36: {p1,p2} c= P2' proof let x;assume x in {p1,p2}; then x=p1 or x=p2 by TARSKI:def 2; hence x in P2' by A6,TOPREAL1:4; end; A37:Q1 \/ {p1,p2}=P1 by A33,XBOOLE_1:45; A38:Q2 \/ {p1,p2}=P2 by A34,XBOOLE_1:45; A39:Q1' \/ {p1,p2}=P1' by A35,XBOOLE_1:45; A40:Q2' \/ {p1,p2}=P2' by A36,XBOOLE_1:45; now assume A41: not(P1=P2' & P2=P1'); now per cases by A41; case A42:P1<>P2'; A43: now assume A44:Q1\Q2'={} & Q2'\Q1={}; then A45:Q1 c= Q2' by XBOOLE_1:37; Q2' c= Q1 by A44,XBOOLE_1:37; hence contradiction by A37,A40,A42,A45,XBOOLE_0:def 10; end; now per cases by A43; case A46:Q1\Q2'<>{}; consider y being Element of Q1\Q2'; A47:y in Q1 by A46,XBOOLE_0:def 4; then A48:y in Q1' \/ Q2' by A23,A24,XBOOLE_0:def 2; not y in Q2' by A46,XBOOLE_0:def 4; then y in Q1' by A48,XBOOLE_0:def 2; then Q1 /\ Q1'<>{} by A47,XBOOLE_0:def 3; then A49:Q1 meets Q1' by XBOOLE_0:def 7; now assume Q2 meets Q1'; then A50:Q1 \/ Q1' \/ Q2 is connected by A29,A30,A31,A49,JORDAN1:7; Q1 \/ Q1' \/ Q2=P\{p1,p2} by A23,A25,XBOOLE_1:4; hence contradiction by A1,A8,A13,A14,A50,Th60; end; then A51: Q2/\Q1'={} by XBOOLE_0:def 7; Q2 c= Q2' proof let x;assume A52:x in Q2; then x in Q1 \/ Q2 by XBOOLE_0:def 2; then x in Q1' or x in Q2' by A23,A24,XBOOLE_0:def 2; hence x in Q2' by A51,A52,XBOOLE_0:def 3; end; then A53: P2 c= P2' by A38,A40,XBOOLE_1:9; Q1' c= Q1 proof let x;assume A54:x in Q1'; then x in Q1 \/ Q2 by A23,A24,XBOOLE_0:def 2; then x in Q1 or x in Q2 by XBOOLE_0:def 2; hence x in Q1 by A51,A54,XBOOLE_0:def 3; end; then P1' c= P1 by A37,A39,XBOOLE_1:9; hence P1=P1' & P2=P2' or P1=P2' & P2=P1' by A2,A3,A5,A6,A53,Th59; case A55:Q2'\Q1<>{}; consider y being Element of Q2'\Q1; A56:y in Q2' by A55,XBOOLE_0:def 4; then A57:y in Q2 \/ Q1 by A23,A24,XBOOLE_0:def 2; not y in Q1 by A55,XBOOLE_0:def 4; then y in Q2 by A57,XBOOLE_0:def 2; then Q2' /\ Q2<>{} by A56,XBOOLE_0:def 3; then A58:Q2' meets Q2 by XBOOLE_0:def 7; now assume Q1' meets Q2; then A59:Q2' \/ Q2 \/ Q1' is connected by A30,A31,A32,A58,JORDAN1:7; Q2' \/ Q2 \/ Q1'=P\{p1,p2} by A24,A28,XBOOLE_1:4; hence contradiction by A1,A8,A13,A14,A59,Th60; end; then A60: Q1'/\Q2={} by XBOOLE_0:def 7; Q1' c= Q1 proof let x;assume A61:x in Q1'; then x in Q1' \/ Q2' by XBOOLE_0:def 2; then x in Q1 or x in Q2 by A23,A24,XBOOLE_0:def 2; hence x in Q1 by A60,A61,XBOOLE_0:def 3; end; then A62: P1' c= P1 by A37,A39,XBOOLE_1:9; Q2 c= Q2' proof let x;assume A63:x in Q2; then x in Q2 \/ Q1 by XBOOLE_0:def 2; then x in Q2' or x in Q1' by A23,A24,XBOOLE_0:def 2; hence x in Q2' by A60,A63,XBOOLE_0:def 3; end; then P2 c= P2' by A38,A40,XBOOLE_1:9; hence P1=P1' & P2=P2' or P1=P2' & P2=P1' by A2,A3,A5,A6,A62,Th59; end; hence P1=P1' & P2=P2' or P1=P2' & P2=P1'; case A64: P2<>P1'; A65: now assume A66:Q2\Q1'={} & Q1'\Q2={}; then A67:Q2 c= Q1' by XBOOLE_1:37; Q1' c= Q2 by A66,XBOOLE_1:37; hence contradiction by A38,A39,A64,A67,XBOOLE_0:def 10; end; now per cases by A65; case A68:Q2\Q1'<>{}; consider y being Element of Q2\Q1'; A69:y in Q2 by A68,XBOOLE_0:def 4; then A70:y in Q2' \/ Q1' by A23,A24,XBOOLE_0:def 2; not y in Q1' by A68,XBOOLE_0:def 4; then y in Q2' by A70,XBOOLE_0:def 2; then Q2 /\ Q2'<>{} by A69,XBOOLE_0:def 3; then A71:Q2 meets Q2' by XBOOLE_0:def 7; now assume Q1 meets Q2'; then A72:Q2 \/ Q2' \/ Q1 is connected by A29,A30,A32,A71,JORDAN1:7; Q2 \/ Q2' \/ Q1=P\{p1,p2} by A23,A26,XBOOLE_1:4; hence contradiction by A1,A8,A13,A14,A72,Th60; end; then A73: Q1/\Q2'={} by XBOOLE_0:def 7; Q1 c= Q1' proof let x;assume A74:x in Q1; then x in Q2 \/ Q1 by XBOOLE_0:def 2; then x in Q2' or x in Q1' by A23,A24,XBOOLE_0:def 2; hence x in Q1' by A73,A74,XBOOLE_0:def 3; end; then A75: P1 c= P1' by A37,A39,XBOOLE_1:9; Q2' c= Q2 proof let x;assume A76:x in Q2'; then x in Q2 \/ Q1 by A23,A24,XBOOLE_0:def 2; then x in Q2 or x in Q1 by XBOOLE_0:def 2; hence x in Q2 by A73,A76,XBOOLE_0:def 3; end; then P2' c= P2 by A38,A40,XBOOLE_1:9; hence P1=P1' & P2=P2' or P1=P2' & P2=P1' by A2,A3,A5,A6,A75,Th59; case A77:Q1'\Q2<>{}; consider y being Element of Q1'\Q2; A78:y in Q1' by A77,XBOOLE_0:def 4; then A79:y in Q1 \/ Q2 by A23,A24,XBOOLE_0:def 2; not y in Q2 by A77,XBOOLE_0:def 4; then y in Q1 by A79,XBOOLE_0:def 2; then Q1' /\ Q1<>{} by A78,XBOOLE_0:def 3; then A80:Q1' meets Q1 by XBOOLE_0:def 7; now assume Q2' meets Q1; then A81:Q1' \/ Q1 \/ Q2' is connected by A29,A31,A32,A80,JORDAN1:7; Q1' \/ Q1 \/ Q2'=P\{p1,p2} by A24,A27,XBOOLE_1:4; hence contradiction by A1,A8,A13,A14,A81,Th60; end; then A82: Q2' /\ Q1 = {} by XBOOLE_0:def 7; Q2' c= Q2 proof let x;assume A83:x in Q2'; then x in Q2' \/ Q1' by XBOOLE_0:def 2; then x in Q2 or x in Q1 by A23,A24,XBOOLE_0:def 2; hence x in Q2 by A82,A83,XBOOLE_0:def 3; end; then A84: P2' c= P2 by A38,A40,XBOOLE_1:9; Q1 c= Q1' proof let x;assume A85:x in Q1; then x in Q1' \/ Q2' by A23,A24,XBOOLE_0:def 2; then x in Q1' or x in Q2' by XBOOLE_0:def 2; hence x in Q1' by A82,A85,XBOOLE_0:def 3; end; then P1 c= P1' by A37,A39,XBOOLE_1:9; hence P1=P1' & P2=P2' or P1=P2' & P2=P1' by A2,A3,A5,A6,A84,Th59; end; hence P1=P1' & P2=P2' or P1=P2' & P2=P1'; end; hence P1=P1' & P2=P2' or P1=P2' & P2=P1'; end; hence thesis; end; begin ::Lower Arcs and Upper Arcs definition cluster -> real Element of R^1; coherence by TOPMETR:24,XREAL_0:def 1; end; Lm1: for g being map of I[01],R^1, s1,s2,r being Real st g is continuous & g.0[01] < r & r < g.1[01] & s1=g.0 & s2=g.1 ex r1 st 0<r1 & r1<1 & g.r1=r proof let g be map of I[01],R^1,s1,s2,r be Real; assume g is continuous & g.0[01] < r & r < g.1[01] & s1=g.0 & s2=g.1; then ex rc being Real st g.rc=r & 0<rc & rc <1 by BORSUK_1:def 17,def 18,TOPMETR:27,TOPREAL5:12; hence thesis; end; canceled 2; theorem Th64: for P1 being Subset of TOP-REAL 2, r being Real,p1,p2 being Point of TOP-REAL 2 st p1`1<=r & r<=p2`1 & P1 is_an_arc_of p1,p2 holds P1 meets Vertical_Line(r) & P1 /\ Vertical_Line(r) is closed proof let P1 be Subset of TOP-REAL 2, r be Real, p1,p2 be Point of TOP-REAL 2; assume A1: p1`1<=r & r<=p2`1 & P1 is_an_arc_of p1,p2; then reconsider P1' = P1 as non empty Subset of TOP-REAL 2 by TOPREAL1:4; consider f being map of I[01], (TOP-REAL 2)|P1' such that A2: f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2; [#]((TOP-REAL 2)|P1)=P1 by PRE_TOPC:def 10; then A3:the carrier of (TOP-REAL 2)|P1=P1 by PRE_TOPC:12; then reconsider f1=f as Function of the carrier of I[01], the carrier of TOP-REAL 2 by FUNCT_2:9; reconsider f2=f1 as map of I[01],TOP-REAL 2 ; reconsider proj11=proj1 as Function of the carrier of TOP-REAL 2,REAL; reconsider proj12=proj1 as map of TOP-REAL 2,R^1 by TOPMETR:24; reconsider g1=proj11*f1 as Function of the carrier of I[01],REAL; reconsider g=g1 as map of I[01],R^1 by TOPMETR:24; f is continuous by A2,TOPS_2:def 5; then A4:f2 is continuous by Th4; proj12 is continuous by TOPREAL5:16; then A5:g is continuous by A4,TOPS_2:58; A6:dom f=[.0,1.] by BORSUK_1:83,FUNCT_2:def 1; then A7:0 in dom f by TOPREAL5:1; A8:1 in dom f by A6,TOPREAL5:1; A9:g.0=proj1.p1 by A2,A7,FUNCT_1:23 .=p1`1 by PSCOMP_1:def 28; A10: g.1=proj1.p2 by A2,A8,FUNCT_1:23 .=p2`1 by PSCOMP_1:def 28; reconsider P1' as non empty Subset of TOP-REAL 2; A11:P1' is closed by A1,Th12; A12: Vertical_Line(r) is closed by Th33; now per cases by A1,A9,A10,AXIOMS:21,BORSUK_1:def 17,def 18; case g.0=g.1; then A13:g.0=r by A1,A9,A10,AXIOMS:21; A14:0 in dom f by A6,TOPREAL5:1; then A15: f.0 in rng f by FUNCT_1:def 5; then f.0 in P1 by A3; then reconsider p=f.0 as Point of TOP-REAL 2; p`1=proj1.(f.0) by PSCOMP_1:def 28 .=r by A13,A14,FUNCT_1:23; then f.0 in {q where q is Point of TOP-REAL 2: q`1=r}; then f.0 in Vertical_Line(r) by Def6; hence P1 meets Vertical_Line(r) by A3,A15,XBOOLE_0:3; case A16: g.0[01]=r; A17:0 in dom f by A6,TOPREAL5:1; then A18: f.0 in rng f by FUNCT_1:def 5; then f.0 in P1 by A3; then reconsider p=f.0 as Point of TOP-REAL 2; p`1=proj1.(f.0) by PSCOMP_1:def 28 .=r by A16,A17,BORSUK_1:def 17,FUNCT_1:23; then f.0 in {q where q is Point of TOP-REAL 2: q`1=r}; then f.0 in Vertical_Line(r) by Def6; hence P1 meets Vertical_Line(r) by A3,A18,XBOOLE_0:3; case A19: g.1[01]=r; A20:1 in dom f by A6,TOPREAL5:1; then A21: f.1 in rng f by FUNCT_1:def 5; then f.1 in P1 by A3; then reconsider p=f.1 as Point of TOP-REAL 2; p`1=proj1.(f.1) by PSCOMP_1:def 28 .=r by A19,A20,BORSUK_1:def 18,FUNCT_1:23; then f.1 in {q where q is Point of TOP-REAL 2: q`1=r}; then f.1 in Vertical_Line(r) by Def6; hence P1 meets Vertical_Line(r) by A3,A21,XBOOLE_0:3; case g.0[01]< r & r < g.1[01]; then consider r1 such that A22:0<r1 & r1<1 & g.r1=r by A5,A9,A10,Lm1; dom f=[.0,1.] by BORSUK_1:83,FUNCT_2:def 1; then A23:r1 in dom f by A22,TOPREAL5:1; [#]((TOP-REAL 2)|P1)=P1 by PRE_TOPC:def 10; then A24:the carrier of (TOP-REAL 2)|P1=P1 by PRE_TOPC:12; A25: f.r1 in rng f by A23,FUNCT_1:def 5; then f.r1 in P1 by A24; then reconsider p=f.r1 as Point of TOP-REAL 2; p`1=proj1.(f.r1) by PSCOMP_1:def 28 .=r by A22,A23,FUNCT_1:23; then f.r1 in {q where q is Point of TOP-REAL 2: q`1=r}; then f.r1 in Vertical_Line(r) by Def6; hence P1 meets Vertical_Line(r) by A24,A25,XBOOLE_0:3; end; hence thesis by A11,A12,TOPS_1:35; end; Lm2:now let P be compact non empty Subset of TOP-REAL 2; assume A1:P is_simple_closed_curve; let P1,P1' be non empty Subset of TOP-REAL 2; assume A2:( ex P2 being non empty Subset of TOP-REAL 2 st P1 is_an_arc_of W-min(P),E-max(P) & P2 is_an_arc_of E-max(P),W-min(P) & P1 /\ P2={W-min(P),E-max(P)} & P1 \/ P2=P & First_Point(P1,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2) & ( ex P2' being non empty Subset of TOP-REAL 2 st P1' is_an_arc_of W-min(P),E-max(P) & P2' is_an_arc_of E-max(P),W-min(P) & P1' /\ P2'={W-min(P),E-max(P)} & P1' \/ P2'=P & First_Point(P1',W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P2',E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2); then consider P2 being non empty Subset of TOP-REAL 2 such that A3:P1 is_an_arc_of W-min(P),E-max(P) & P2 is_an_arc_of E-max(P),W-min(P) & P1 /\ P2={W-min(P),E-max(P)} & P1 \/ P2=P & First_Point(P1,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2; A4:P2 is_an_arc_of W-min(P),E-max(P) by A3,JORDAN5B:14; consider P2' being non empty Subset of TOP-REAL 2 such that A5:P1' is_an_arc_of W-min(P),E-max(P) & P2' is_an_arc_of E-max(P),W-min(P) & P1' /\ P2'={W-min(P),E-max(P)} & P1' \/ P2'=P & First_Point(P1',W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P2',E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by A2; A6:P2' is_an_arc_of W-min(P),E-max(P) by A5,JORDAN5B:14; now assume A7:P1=P2' & P2=P1'; A8:(W-min(P))`1=W-bound(P) by PSCOMP_1:84; A9:(E-max(P))`1=E-bound(P) by PSCOMP_1:104; then (W-min(P))`1<(E-max(P))`1 by A1,A8,TOPREAL5:23; then A10: (W-min P)`1<=(W-bound(P)+E-bound(P))/2 & (W-bound(P)+E-bound(P))/2<=(E-max P)`1 by A8,A9,TOPREAL3:3; then P2 meets Vertical_Line((W-bound(P)+E-bound(P))/2) & P2 /\ Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by A4,Th64; then A11:First_Point(P1,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> First_Point(P2,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by A3,JORDAN5C:18; P2' meets Vertical_Line((W-bound(P)+E-bound(P))/2) & P2' /\ Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by A6,A10,Th64; hence contradiction by A5,A7,A11,JORDAN5C:18; end; hence P1=P1' by A1,A3,A4,A5,A6,Th61; end; definition let P be compact non empty Subset of TOP-REAL 2 such that A1:P is_simple_closed_curve; func Upper_Arc(P) -> non empty Subset of TOP-REAL 2 means :Def8: it is_an_arc_of W-min(P),E-max(P) & ex P2 being non empty Subset of TOP-REAL 2 st P2 is_an_arc_of E-max(P),W-min(P) & it /\ P2={W-min(P),E-max(P)} & it \/ P2=P & First_Point(it,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2; existence proof ex P1,P2 being non empty Subset of TOP-REAL 2 st P1 is_an_arc_of W-min(P),E-max(P) & P2 is_an_arc_of E-max(P),W-min(P) & P1 /\ P2={W-min(P),E-max(P)} & P1 \/ P2=P & First_Point(P1,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by A1,Th40; hence thesis; end; uniqueness by A1,Lm2; end; definition let P be compact non empty Subset of TOP-REAL 2; assume A1:P is_simple_closed_curve; then A2:Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by Def8; func Lower_Arc(P) -> non empty Subset of TOP-REAL 2 means :Def9: it is_an_arc_of E-max(P),W-min(P) & Upper_Arc(P) /\ it={W-min(P),E-max(P)} & Upper_Arc(P) \/ it=P & First_Point(Upper_Arc(P),W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(it,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2; existence by A1,Def8; uniqueness proof let P1,P1' be non empty Subset of TOP-REAL 2; assume A3:( P1 is_an_arc_of E-max(P),W-min(P) & Upper_Arc(P) /\ P1={W-min(P),E-max(P)} & Upper_Arc(P) \/ P1=P & First_Point(Upper_Arc(P),W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P1,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2) & ( P1' is_an_arc_of E-max(P),W-min(P) & Upper_Arc(P) /\ P1'={W-min(P),E-max(P)} & Upper_Arc(P) \/ P1'=P & First_Point(Upper_Arc(P),W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(P1',E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2); then A4:P1 is_an_arc_of W-min(P),E-max(P) by JORDAN5B:14; P1' is_an_arc_of W-min(P),E-max(P) by A3,JORDAN5B:14; then P1=P1' or Upper_Arc(P)=P1' & P1=Upper_Arc(P) by A1,A2,A3,A4,Th61; hence P1=P1'; end; end; theorem Th65:for P being compact non empty Subset of (TOP-REAL 2) st P is_simple_closed_curve holds Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) & Upper_Arc(P) is_an_arc_of E-max(P),W-min(P) & Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) & Lower_Arc(P) is_an_arc_of W-min(P),E-max(P) & Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)} & Upper_Arc(P) \/ Lower_Arc(P)=P & First_Point(Upper_Arc(P),W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(Lower_Arc(P),E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2 proof let P be compact non empty Subset of (TOP-REAL 2); assume A1:P is_simple_closed_curve; then A2: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by Def8; Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,Def9; hence thesis by A1,A2,Def9,JORDAN5B:14; end; theorem Th66: for P being compact non empty Subset of (TOP-REAL 2) st P is_simple_closed_curve holds Lower_Arc(P)=(P\Upper_Arc(P)) \/ {W-min(P),E-max(P)} & Upper_Arc(P)=(P\Lower_Arc(P)) \/ {W-min(P),E-max(P)} proof let P be compact non empty Subset of (TOP-REAL 2); assume P is_simple_closed_curve; then A1: Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)} & Upper_Arc(P) \/ Lower_Arc(P)=P by Def9; set B=Upper_Arc(P),A=Lower_Arc(P); A2: (B \/ A \B)\/ (B /\ A) =(A \ B) \/ (A/\B) by XBOOLE_1:40 .=A by XBOOLE_1: 51 ; (B \/ A \A)\/ (B /\ A) =(B \ A) \/ (B/\A) by XBOOLE_1:40 .=B by XBOOLE_1:51; hence thesis by A1,A2; end; theorem for P being compact non empty Subset of (TOP-REAL 2), P1 being Subset of (TOP-REAL 2)|P st P is_simple_closed_curve & Upper_Arc(P) /\ P1={W-min(P),E-max(P)} & Upper_Arc(P) \/ P1=P holds P1=Lower_Arc(P) proof let P be compact non empty Subset of (TOP-REAL 2), P1 be Subset of (TOP-REAL 2)|P; assume A1: P is_simple_closed_curve & Upper_Arc(P) /\ P1={W-min(P),E-max(P)} & Upper_Arc(P) \/ P1=P; set B=Upper_Arc(P); (B \/ P1 \B)\/ (B /\ P1) =(P1 \ B) \/ (P1/\B) by XBOOLE_1:40 .=P1 by XBOOLE_1:51; hence thesis by A1,Th66; end; theorem for P being compact non empty Subset of (TOP-REAL 2), P1 being Subset of (TOP-REAL 2)|P st P is_simple_closed_curve & P1 /\ Lower_Arc(P)={W-min(P),E-max(P)} & P1 \/ Lower_Arc(P)=P holds P1=Upper_Arc(P) proof let P be compact non empty Subset of (TOP-REAL 2), P1 be Subset of (TOP-REAL 2)|P; assume A1: P is_simple_closed_curve & P1 /\ Lower_Arc(P)={W-min(P),E-max(P)} & P1 \/ Lower_Arc(P)=P; set B=Lower_Arc(P); (P1 \/ B\B) \/ (P1 /\ B) =P1 /\B \/ (P1\B) by XBOOLE_1:40 .=P1 by XBOOLE_1:51; hence thesis by A1,Th66; end; begin ::An Order of Points in a Simple Closed Curve theorem Th69: for P being Subset of TOP-REAL 2, p1, p2, q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 holds q=p1 proof let P be Subset of TOP-REAL 2, p1, p2, q be Point of TOP-REAL 2; assume A1: P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2; then q in P by JORDAN5C:def 3; then LE p1,q,P,p1,p2 by A1,JORDAN5C:10; hence q=p1 by A1,JORDAN5C:12; end; theorem Th70: for P being Subset of TOP-REAL 2, p1, p2, q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 holds q=p2 proof let P be Subset of TOP-REAL 2, p1, p2, q be Point of TOP-REAL 2; assume A1: P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2; then q in P by JORDAN5C:def 3; then LE q,p2,P,p1,p2 by A1,JORDAN5C:10; hence q=p2 by A1,JORDAN5C:12; end; definition let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2; pred LE q1,q2,P means :Def10: q1 in Upper_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) or q1 in Upper_Arc(P) & q2 in Upper_Arc(P) & LE q1,q2,Upper_Arc(P),W-min(P),E-max(P) or q1 in Lower_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) & LE q1,q2,Lower_Arc(P),E-max(P),W-min(P); end; theorem for P being compact non empty Subset of (TOP-REAL 2), q being Point of TOP-REAL 2 st P is_simple_closed_curve & q in P holds LE q,q,P proof let P be compact non empty Subset of (TOP-REAL 2), q be Point of TOP-REAL 2; assume A1: P is_simple_closed_curve & q in P; then A2:Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) & Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)} & Upper_Arc(P) \/ Lower_Arc(P)=P & First_Point(Upper_Arc(P),W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(Lower_Arc(P),E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by Def9; A3: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,Th65; now per cases by A1,A2,XBOOLE_0:def 2; case A4:q in Upper_Arc(P); then LE q,q,Upper_Arc(P),W-min(P),E-max(P) by A3,JORDAN5C:9; hence LE q,q,P by A4,Def10; case A5:q in Lower_Arc(P) & not q in Upper_Arc(P); then A6:LE q,q,Lower_Arc(P),E-max(P),W-min(P) by A2,JORDAN5C:9; q <> W-min P by A3,A5,TOPREAL1:4; hence LE q,q,P by A5,A6,Def10; end; hence LE q,q,P; end; theorem for P being compact non empty Subset of TOP-REAL 2, q1,q2 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds q1=q2 proof let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2; assume A1: P is_simple_closed_curve & LE q1,q2,P & LE q2,q1,P; then A2: Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) & Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)} & Upper_Arc(P) \/ Lower_Arc(P)=P & First_Point(Upper_Arc(P),W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(Lower_Arc(P),E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by Def9; A3: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,Th65; now per cases by A1,Def10; case A4:q1 in Upper_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P); now per cases by A1,Def10; case A5: q2 in Upper_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P); then q1 in Upper_Arc(P) /\ Lower_Arc(P) by A4,XBOOLE_0:def 3; then A6:q1=E-max(P) by A2,A5,TARSKI:def 2; q2 in Upper_Arc(P) /\ Lower_Arc(P) by A4,A5,XBOOLE_0:def 3; hence q1=q2 by A2,A4,A6,TARSKI:def 2; case A7: q2 in Upper_Arc(P) & q1 in Upper_Arc(P) & LE q2,q1,Upper_Arc(P),W-min(P),E-max(P); then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A4,XBOOLE_0:def 3; then q2=E-max(P) by A2,A4,TARSKI:def 2; hence q1=q2 by A3,A7,Th70; case A8: q2 in Lower_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P) & LE q2,q1,Lower_Arc(P),E-max(P),W-min(P); then q1 in Upper_Arc(P) /\ Lower_Arc(P) by A4,XBOOLE_0:def 3; then q1=E-max(P) by A2,A8,TARSKI:def 2; hence q1=q2 by A2,A8,Th69; end; hence q1=q2; case A9:q1 in Upper_Arc(P) & q2 in Upper_Arc(P) & LE q1,q2,Upper_Arc(P),W-min(P),E-max(P); now per cases by A1,Def10; case A10: q2 in Upper_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P); then q1 in Upper_Arc(P) /\ Lower_Arc(P) by A9,XBOOLE_0:def 3; then q1=E-max(P) by A2,A10,TARSKI:def 2; hence q1=q2 by A3,A9,Th70; case q2 in Upper_Arc(P) & q1 in Upper_Arc(P) & LE q2,q1,Upper_Arc(P),W-min(P),E-max(P); hence q1=q2 by A3,A9,JORDAN5C:12; case A11: q2 in Lower_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P) & LE q2,q1,Lower_Arc(P),E-max(P),W-min(P); then q1 in Upper_Arc(P) /\ Lower_Arc(P) by A9,XBOOLE_0:def 3; then q1=E-max(P) by A2,A11,TARSKI:def 2; hence q1=q2 by A2,A11,Th69; end; hence q1=q2; case A12:q1 in Lower_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) & LE q1,q2,Lower_Arc(P),E-max(P),W-min(P); now per cases by A1,Def10; case q2 in Upper_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P); then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A12,XBOOLE_0:def 3; then q2=E-max(P) by A2,A12,TARSKI:def 2; hence q1=q2 by A2,A12,Th69; case A13: q2 in Upper_Arc(P) & q1 in Upper_Arc(P) & LE q2,q1,Upper_Arc(P),W-min(P),E-max(P); then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A12,XBOOLE_0:def 3; then q2=E-max(P) by A2,A12,TARSKI:def 2; hence q1=q2 by A3,A13,Th70; case q2 in Lower_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P) & LE q2,q1,Lower_Arc(P),E-max(P),W-min(P); hence q1=q2 by A2,A12,JORDAN5C:12; end; hence q1=q2; end; hence q1=q2; end; theorem for P being compact non empty Subset of TOP-REAL 2, q1,q2,q3 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P holds LE q1,q3,P proof let P be compact non empty Subset of TOP-REAL 2, q1,q2,q3 be Point of TOP-REAL 2; assume A1: P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P; then A2: Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) & Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)} & Upper_Arc(P) \/ Lower_Arc(P)=P & First_Point(Upper_Arc(P),W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2> Last_Point(Lower_Arc(P),E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by Def9; A3: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,Th65; now per cases by A1,Def10; case A4:q1 in Upper_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P); now per cases by A1,Def10; case q2 in Upper_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P); hence LE q1,q3,P by A4,Def10; case A5: q2 in Upper_Arc(P) & q3 in Upper_Arc(P) & LE q2,q3,Upper_Arc(P),W-min(P),E-max(P); then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A4,XBOOLE_0:def 3; then q2=E-max(P) by A2,A4,TARSKI:def 2; hence LE q1,q3,P by A1,A3,A5,Th70; case q2 in Lower_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P) & LE q2,q3,Lower_Arc(P),E-max(P),W-min(P); hence LE q1,q3,P by A4,Def10; end; hence LE q1,q3,P; case A6:q1 in Upper_Arc(P) & q2 in Upper_Arc(P) & LE q1,q2,Upper_Arc(P),W-min(P),E-max(P); now per cases by A1,Def10; case q2 in Upper_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P); hence LE q1,q3,P by A6,Def10; case A7: q2 in Upper_Arc(P) & q3 in Upper_Arc(P) & LE q2,q3,Upper_Arc(P),W-min(P),E-max(P); then LE q1,q3,Upper_Arc(P),W-min(P),E-max(P) by A3,A6,JORDAN5C:13; hence LE q1,q3,P by A6,A7,Def10; case q2 in Lower_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P) & LE q2,q3,Lower_Arc(P),E-max(P),W-min(P); hence LE q1,q3,P by A6,Def10; end; hence LE q1,q3,P; case A8:q1 in Lower_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) & LE q1,q2,Lower_Arc(P),E-max(P),W-min(P); now per cases by A1,Def10; case A9: q2 in Upper_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P); then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A8,XBOOLE_0:def 3; then q2=E-max(P) by A2,A8,TARSKI:def 2; then LE q2,q3,Lower_Arc(P),E-max(P),W-min(P) by A2,A9,JORDAN5C:10; then LE q1,q3,Lower_Arc(P),E-max(P),W-min(P) by A2,A8,JORDAN5C:13; hence LE q1,q3,P by A8,A9,Def10; case A10: q2 in Upper_Arc(P) & q3 in Upper_Arc(P) & LE q2,q3,Upper_Arc(P),W-min(P),E-max(P); then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A8,XBOOLE_0:def 3; then q2=E-max(P) by A2,A8,TARSKI:def 2; hence LE q1,q3,P by A1,A3,A10,Th70; case A11: q2 in Lower_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P) & LE q2,q3,Lower_Arc(P),E-max(P),W-min(P); then LE q1,q3,Lower_Arc(P),E-max(P),W-min(P) by A2,A8,JORDAN5C:13; hence LE q1,q3,P by A8,A11,Def10; end; hence LE q1,q3,P; end; hence LE q1,q3,P; end;

Back to top