0 by XREAL_1:50; then 1-a+a>=0+a by A10,A11,XREAL_1:7; then q in LSeg(f/.j,p) by A10,A13,A15; then LE q,p,L~f,f/.1,f/.(len f) by A1,A2,A3,SPRECT_3:23; hence contradiction by A7,A16,JORDAN5C:12,TOPREAL1:25; end; hence thesis; end; suppose p`1=(f/.j)`1; hence thesis by A4,A6,A8,TOPREAL1:3; end; end; theorem Th7: for f being S-Sequence_in_R2, p,q being Point of TOP-REAL 2 st 1 <=j & j < len f & p in LSeg(f,j) & q in LSeg(f,j) & (f/.j)`2=(f/.(j+1))`2 & (f /.j)`1<(f/.(j+1))`1 & LE p,q,L~f,f/.1,f/.(len f) holds p`1<=q`1 proof let f be S-Sequence_in_R2, p,q be Point of TOP-REAL 2; assume that A1: 1 <=j and A2: j < len f and A3: p in LSeg(f,j) and A4: q in LSeg(f,j) and A5: (f/.j)`2=(f/.(j+1))`2 and A6: (f/.j)`1<(f/.(j+1))`1 and A7: LE p,q,L~f,f/.1,f/.(len f); j+1<=len f by A2,NAT_1:13; then A8: LSeg(f,j)=LSeg(f/.j,f/.(j+1)) by A1,TOPREAL1:def 3; per cases; suppose A9: p`1<> (f/.(j))`1; (f/.j)`1<=p`1 by A3,A6,A8,TOPREAL1:3; then (f/.(j))`1q`1; then q`1-p`1<0 by XREAL_1:49; then 1-a+a>=0+a by A10,A11,XREAL_1:7; then q in LSeg(f/.(j),p) by A10,A13,A15; then LE q,p,L~f,f/.1,f/.(len f) by A1,A2,A3,SPRECT_3:23; hence contradiction by A7,A16,JORDAN5C:12,TOPREAL1:25; end; hence thesis; end; suppose p`1=(f/.(j))`1; hence thesis by A4,A6,A8,TOPREAL1:3; end; end; definition let P be Subset of TOP-REAL 2, p1,p2,p be Point of TOP-REAL 2, e be Real; pred p is_Lin P,p1,p2,e means P is_an_arc_of p1,p2 & p in P & p`1=e & ex p4 being Point of TOP-REAL 2 st p4`1

e & LE p4,p,P,p1,p2 & for p5 being Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5,p,P,p1,p2 holds p5`1>=e; pred p is_Lout P,p1,p2,e means P is_an_arc_of p1,p2 & p in P & p`1=e & ex p4 being Point of TOP-REAL 2 st p4`1 e & LE p,p4,P,p1,p2 & for p5 being Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE p,p5,P,p1,p2 holds p5`1>=e; pred p is_OSin P,p1,p2,e means P is_an_arc_of p1,p2 & p in P & p`1=e & ex p7 being Point of TOP-REAL 2 st LE p7,p,P,p1,p2 & (for p8 being Point of TOP-REAL 2 st LE p7,p8,P,p1,p2 & LE p8,p,P,p1,p2 holds p8`1=e) & for p4 being Point of TOP-REAL 2 st LE p4,p7,P,p1,p2 & p4<>p7 holds (ex p5 being Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5,p7,P,p1,p2 & p5`1>e) & ex p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6,p7,P,p1,p2 & p6`1 p7 holds (ex p5 being Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE p7,p5,P,p1,p2 & p5`1>e)& ex p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p7,p6,P,p1,p2 & p6`1 =e holds ex p3 being Point of TOP-REAL 2 st p3 in P & p3`1=e proof let P be Subset of TOP-REAL 2, p1,p2,p be Point of TOP-REAL 2,e be Real; set x = the Element of P /\ Vertical_Line(e); assume P is_an_arc_of p1,p2 & p1`1<=e & p2`1>=e; then P meets Vertical_Line(e) by JORDAN6:49; then A1: P /\ Vertical_Line(e) <> {} by XBOOLE_0:def 7; then x in Vertical_Line(e) by XBOOLE_0:def 4; then x in {p3 where p3 is Point of TOP-REAL 2: p3`1=e} by JORDAN6:def 6; then A2: ex p4 being Point of TOP-REAL 2 st p4=x & p4`1=e; x in P by A1,XBOOLE_0:def 4; hence thesis by A2; end; theorem for P being non empty Subset of TOP-REAL 2, p1,p2,p being Point of TOP-REAL 2,e being Real st P is_an_arc_of p1,p2 & p1`1 e by A2,A6; then A15: 0 in {s where s is Element of REAL: 0<=s & s<=s2 & (for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e)} by A13,A14; {s where s is Element of REAL: 0<=s & s<=s2 & for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e } c= REAL proof let x be object; assume x in {s where s is Element of REAL: 0<=s & s<=s2 & (for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e)}; then ex s being Element of REAL st s=x & 0<=s & s<=s2 & for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e; hence thesis; end; then reconsider R={s where s is Element of REAL: 0<=s & s<=s2 & (for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e)} as non empty Subset of REAL by A15; A16: s2<=1 by A10,BORSUK_1:40,XXREAL_1:1; R c= [.0,1.] proof let x be object; assume x in R; then consider s being Element of REAL such that A17: s=x & 0<=s and A18: s<=s2 and for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e; s<=1 by A16,A18,XXREAL_0:2; hence thesis by A17,XXREAL_1:1; end; then reconsider R99=R as Subset of I[01] by BORSUK_1:40; reconsider s0=upper_bound R as Element of REAL by XREAL_0:def 1; A19: for s being Real st s in R holds s < s2 proof let s be Real; assume s in R; then A20: ex s3 being Element of REAL st s3=s & 0<=s3 & s3<=s2 & for q being Point of TOP-REAL 2 st q=f.s3 holds q`1<>e; then s<>s2 by A4,A11; hence thesis by A20,XXREAL_0:1; end; then for s being Real st s in R holds s <= s2; then A21: s0 <= s2 by SEQ_4:45; then A22: s0 <=1 by A16,XXREAL_0:2; R99=R; then A23: 0 <= s0 by A15,BORSUK_4:26; then s0 in dom f by A12,A22,BORSUK_1:40,XXREAL_1:1; then f.s0 in rng f by FUNCT_1:def 3; then f.s0 in P by A9,PRE_TOPC:def 5; then reconsider p9=f.s0 as Point of TOP-REAL 2; A24: LE p9,p,P,p1,p2 by A1,A5,A6,A7,A11,A16,A23,A21,A22,JORDAN5C:8; for p7 being Point of (TOP-REAL 2)|P holds pro1.p7=proj1.p7 proof let p7 be Point of (TOP-REAL 2)|P; the carrier of ((TOP-REAL 2)|P)=P by PRE_TOPC:8; hence thesis by FUNCT_1:49; end; then A25: pro1 is continuous by JGRAPH_2:29; reconsider h=pro1*f as Function of I[01],R^1; A26: dom h=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1; for s being ExtReal st s in R holds s <= s2 by A19; then s2 is UpperBound of R by XXREAL_2:def 1; then A27: R is bounded_above by XXREAL_2:def 10; A28: rng f=P by A9,PRE_TOPC:def 5; A29: for p8 being Point of TOP-REAL 2 st LE p9,p8,P,p1,p2 & LE p8,p,P,p1, p2 holds p8`1=e proof let p8 be Point of TOP-REAL 2; assume that A30: LE p9,p8,P,p1,p2 and A31: LE p8,p,P,p1,p2; A32: p8 in P by A30,JORDAN5C:def 3; then consider x8 being object such that A33: x8 in dom f and A34: p8=f.x8 by A28,FUNCT_1:def 3; reconsider s8=x8 as Element of REAL by A12,A33,BORSUK_1:40; A35: s8<=1 by A33,BORSUK_1:40,XXREAL_1:1; then A36: s8<=s2 by A5,A6,A7,A11,A13,A16,A31,A34,JORDAN5C:def 3; A37: 0<=s8 by A33,BORSUK_1:40,XXREAL_1:1; then A38: s0 <=s8 by A5,A6,A7,A22,A30,A34,A35,JORDAN5C:def 3; now reconsider s8n=s8 as Point of RealSpace by METRIC_1:def 13; reconsider s8m=s8 as Point of Closed-Interval-MSpace(0,1) by A33, BORSUK_1:40,TOPMETR:10; reconsider ee=|.p8`1-e.|/2 as Real; reconsider w=p8`1 as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1; reconsider B=Ball(w,ee) as Subset of R^1 by METRIC_1:def 13,TOPMETR:17; A39: B={s7 where s7 is Real:p8`1-ee e; then p8`1-e<>0; then |.p8`1-e.|>0 by COMPLEX1:47; then A41: w in Ball(w,ee) by GOBOARD6:1,XREAL_1:139; A42: h"B is open & I[01]=TopSpaceMetr(Closed-Interval-MSpace(0,1)) by A8,A25 ,TOPMETR:20,def 6,def 7,UNIFORM1:2; h.s8=pro1.(f.s8) by A26,A33,BORSUK_1:40,FUNCT_1:12 .=proj1.p8 by A32,A34,FUNCT_1:49 .=p8`1 by PSCOMP_1:def 5; then s8 in h"B by A26,A33,A41,BORSUK_1:40,FUNCT_1:def 7; then consider r0 being Real such that A43: r0>0 and A44: Ball(s8m,r0) c= h"B by A42,TOPMETR:15; reconsider r0 as Real; reconsider r01=min(s2-s8,r0) as Real; s8 0 by XREAL_1:50; then A45: r01>0 by A43,XXREAL_0:21; then A46: r01-r01/2+r01/2>0+r01/2 by XREAL_1:6; then A47: s8+r01/2 =r01 by XXREAL_0:17; then A49: s2-s8+s8>=r01+s8 by XREAL_1:7; then A50: s70<=s2 by A47,XXREAL_0:2; s8+r01<=1 by A16,A49,XXREAL_0:2; then s8+r01/2<1 by A47,XXREAL_0:2; then A51: s8+r01/2 in [.0,1.] by A37,A45,XXREAL_1:1; Ball(s8m,r01) c= Ball(s8m,r0) by PCOMPS_1:1,XXREAL_0:17; then A52: (].s8-r01,s8+r01 .[)/\ [.0,1.] c= h"B by A44,A48; s8+0 e proof let p7 be Point of TOP-REAL 2; assume A58: p7=f.s70; s70<=1 by A16,A50,XXREAL_0:2; then s70 in [.0,1.] by A37,A45,XXREAL_1:1; then A59: p7 in rng f by A12,A58,BORSUK_1:40,FUNCT_1:def 3; A60: rng f=[#]((TOP-REAL 2)|P) by A5,TOPS_2:def 5 .=P by PRE_TOPC:def 5; A61: h.s70=pro1.(f.s70) by A56,FUNCT_1:12 .=pr1a.(p7) by A58,A59,A60,FUNCT_1:49 .=p7`1 by PSCOMP_1:def 5; then A62: p7`1 =0; then p8`1-(p8`1-e)/2 =0/2 by A65; hence contradiction by A66; end; case A67: p8`1-e<0; then e< p8`1+(-(p8`1-e))/2 by A62,A64,ABSVALUE:def 1; then p8`1/2+e/2>e/2+e/2; then p8`1/2>e/2 by XREAL_1:7; then A68: p8`1/2-e/2>e/2-e/2 by XREAL_1:14; (p8`1-e)/2<=0/2 by A67; hence contradiction by A68; end; end; hence contradiction; end; hence thesis; end; s8 e by A37,A50,A57; reconsider s7 as Element of REAL by XREAL_0:def 1; s7 in R by A70; then s7 <= s0 by A27,SEQ_4:def 1; hence contradiction by A38,A69,XXREAL_0:2; end; hence thesis; end; assume not p is_OSin P,p1,p2,e; then consider p4 being Point of TOP-REAL 2 such that A71: LE p4,p9,P,p1,p2 and A72: p4<>p9 and A73: (for p5 being Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5,p9 , P,p1,p2 holds p5`1<=e)or for p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6,p9,P,p1,p2 holds p6`1>=e by A1,A3,A4,A24,A29; A74: p9 in P by A71,JORDAN5C:def 3; now per cases by A73; case A75: for p5 being Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5 ,p9,P,p1,p2 holds p5`1<=e; A76: now p4 in P by A71,JORDAN5C:def 3; then p4 in rng f by A9,PRE_TOPC:def 5; then consider xs4 being object such that A77: xs4 in dom f and A78: p4=f.xs4 by FUNCT_1:def 3; reconsider s4=xs4 as Real by A77; A79: 0<=s4 by A77,BORSUK_1:40,XXREAL_1:1; A80: s4<=1 by A77,BORSUK_1:40,XXREAL_1:1; assume A81: not ex p51 being Point of TOP-REAL 2 st LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 & p51`1 =e & p51`1<=e by A75,A81; hence thesis by XXREAL_0:1; end; A83: now assume s4< s0; then A84: s0-s4>0 by XREAL_1:50; then A85: s4 0 by A84,XREAL_1:139; then consider r being Real such that A86: r in R and A87: s0-((s0-s4)/2) e by A86; then A89: r<=1 by A16,XXREAL_0:2; then r in [.0,1.] by A79,A85,A87,XXREAL_1:1; then f.rss in rng f by A12,BORSUK_1:40,FUNCT_1:def 3; then f.rss in P by A9,PRE_TOPC:def 5; then reconsider pss=f.rss as Point of TOP-REAL 2; s4 =e; A101: now p4 in P by A71,JORDAN5C:def 3; then p4 in rng f by A9,PRE_TOPC:def 5; then consider xs4 being object such that A102: xs4 in dom f and A103: p4=f.xs4 by FUNCT_1:def 3; reconsider s4=xs4 as Real by A102; A104: 0<=s4 by A102,BORSUK_1:40,XXREAL_1:1; A105: s4<=1 by A102,BORSUK_1:40,XXREAL_1:1; assume A106: not ex p51 being Point of TOP-REAL 2 st LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 & p51`1>e; A107: for p51 being Point of TOP-REAL 2 st LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 holds p51`1=e proof let p51 be Point of TOP-REAL 2; assume LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2; then p51`1<=e & p51`1>=e by A100,A106; hence thesis by XXREAL_0:1; end; A108: now assume s4 0 by XREAL_1:50; then A110: s4 0 by A109,XREAL_1:139; then consider r being Real such that A111: r in R and A112: s0-((s0-s4)/2) e by A111; then A114: r<=1 by A16,XXREAL_0:2; then r in [.0,1.] by A104,A110,A112,XXREAL_1:1; then f.rss in rng f by A12,BORSUK_1:40,FUNCT_1:def 3; then f.rss in P by A9,PRE_TOPC:def 5; then reconsider pss=f.rss as Point of TOP-REAL 2; s4 e; then consider p51 being Point of TOP-REAL 2 such that A116: LE p4,p51,P,p1,p2 and A117: LE p51,p9,P,p1,p2 and A118: p51`1>e; A119: for p5 being Point of TOP-REAL 2 st LE p51,p5,P,p1,p2 & LE p5, p,P,p1,p2 holds p5`1>=e proof let p5 be Point of TOP-REAL 2; assume that A120: LE p51,p5,P,p1,p2 and A121: LE p5,p,P,p1,p2; A122: LE p4,p5,P,p1,p2 by A116,A120,JORDAN5C:13; A123: p5 in P by A120,JORDAN5C:def 3; then A124: p5=p9 implies LE p9,p5,P,p1,p2 by JORDAN5C:9; now per cases by A1,A74,A123,A124,JORDAN5C:14; case LE p5,p9,P,p1,p2; hence thesis by A100,A122; end; case LE p9,p5,P,p1,p2; hence thesis by A29,A121; end; end; hence thesis; end; LE p51,p,P,p1,p2 by A24,A117,JORDAN5C:13; hence p is_Rin P,p1,p2,e by A1,A3,A4,A118,A119; end; hence p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e by A101; end; end; hence p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e; end; hence thesis; end; theorem for P being non empty Subset of TOP-REAL 2, p1,p2,p being Point of TOP-REAL 2,e being Real st P is_an_arc_of p1,p2 & p2`1>e & p in P & p`1=e holds p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e or p is_OSout P,p1,p2,e proof let P be non empty Subset of TOP-REAL 2, p1,p2,p be Point of TOP-REAL 2,e be Real; assume that A1: P is_an_arc_of p1,p2 and A2: p2`1>e and A3: p in P and A4: p`1=e; now reconsider pr1a=proj1 as Function of TOP-REAL 2,R^1 by TOPMETR:17; reconsider pro1=pr1a|P as Function of (TOP-REAL 2)|P,R^1 by PRE_TOPC:9; consider f being Function of I[01], (TOP-REAL 2)|P such that A5: f is being_homeomorphism and A6: f.0 = p1 and A7: f.1 = p2 by A1,TOPREAL1:def 1; A8: f is continuous by A5,TOPS_2:def 5; A9: rng f=[#]((TOP-REAL 2)|P) by A5,TOPS_2:def 5; then p in rng f by A3,PRE_TOPC:def 5; then consider xs being object such that A10: xs in dom f and A11: p=f.xs by FUNCT_1:def 3; A12: dom f=[#](I[01]) by A5,TOPS_2:def 5; reconsider s2=xs as Real by A10; A13: s2<=1 by A10,BORSUK_1:40,XXREAL_1:1; for q being Point of TOP-REAL 2 st q=f.1 holds q`1<>e by A2,A7; then A14: 1 in {s where s is Real: 1>=s & s>=s2 & (for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e)} by A13; {s where s is Real: 1>=s & s>=s2 & for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e } c= REAL proof let x be object; assume x in {s where s is Real: 1>=s & s>=s2 & (for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e)}; then consider s being Real such that A15: s=x & 1>=s & s>=s2 & for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e; s in REAL by XREAL_0:def 1; hence thesis by A15; end; then reconsider R={s where s is Real: 1>=s & s>=s2 & (for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e)} as non empty Subset of REAL by A14; reconsider s0=lower_bound R as Real; A16: for s being Real st s in R holds s > s2 proof let s be Real; assume s in R; then A17: ex s3 being Real st s3=s & 1>=s3 & s3>=s2 & for q being Point of TOP-REAL 2 st q=f.s3 holds q`1<>e; then s<>s2 by A4,A11; hence thesis by A17,XXREAL_0:1; end; then for s being Real st s in R holds s >= s2; then A18: s0 >= s2 by SEQ_4:43; for p7 being Point of (TOP-REAL 2)|P holds pro1.p7=proj1.p7 proof let p7 be Point of (TOP-REAL 2)|P; the carrier of ((TOP-REAL 2)|P)=P by PRE_TOPC:8; hence thesis by FUNCT_1:49; end; then A19: pro1 is continuous by JGRAPH_2:29; reconsider h=pro1*f as Function of I[01],R^1; A20: dom h=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1; for s being ExtReal st s in R holds s >= s2 by A16; then s2 is LowerBound of R by XXREAL_2:def 2; then A21: R is bounded_below by XXREAL_2:def 9; A22: 0<=s2 by A10,BORSUK_1:40,XXREAL_1:1; R c= [.0,1.] proof let x be object; assume x in R; then ex s being Real st s=x & 1>=s & s>=s2 & for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e; hence thesis by A22,XXREAL_1:1; end; then A23: 1 >= s0 by A14,BORSUK_1:40,BORSUK_4:26; then s0 in dom f by A12,A22,A18,BORSUK_1:40,XXREAL_1:1; then f.s0 in rng f by FUNCT_1:def 3; then f.s0 in P by A9,PRE_TOPC:def 5; then reconsider p9=f.s0 as Point of TOP-REAL 2; A24: LE p,p9,P,p1,p2 by A1,A5,A6,A7,A11,A22,A13,A23,A18,JORDAN5C:8; A25: rng f=P by A9,PRE_TOPC:def 5; A26: for p8 being Point of TOP-REAL 2 st LE p8,p9,P,p1,p2 & LE p,p8,P,p1, p2 holds p8`1=e proof let p8 be Point of TOP-REAL 2; assume that A27: LE p8,p9,P,p1,p2 and A28: LE p,p8,P,p1,p2; A29: p8 in P by A27,JORDAN5C:def 3; then consider x8 being object such that A30: x8 in dom f and A31: p8=f.x8 by A25,FUNCT_1:def 3; reconsider s8=x8 as Element of REAL by A12,A30,BORSUK_1:40; A32: s8<=1 by A30,BORSUK_1:40,XXREAL_1:1; 0<=s8 by A30,BORSUK_1:40,XXREAL_1:1; then A33: s8>=s2 by A5,A6,A7,A11,A13,A28,A31,A32,JORDAN5C:def 3; A34: s0>=s8 by A5,A6,A7,A22,A23,A18,A27,A31,A32,JORDAN5C:def 3; now reconsider s8n=s8 as Point of RealSpace by METRIC_1:def 13; reconsider s8m=s8 as Point of Closed-Interval-MSpace(0,1) by A30, BORSUK_1:40,TOPMETR:10; reconsider ee=|.p8`1-e.|/2 as Real; reconsider w=p8`1 as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1; reconsider B=Ball(w,ee) as Subset of R^1 by METRIC_1:def 13,TOPMETR:17; A35: B={s7 where s7 is Real:p8`1-ee e; then p8`1-e<>0; then |.p8`1-e.|>0 by COMPLEX1:47; then A37: w in Ball(w,ee) by GOBOARD6:1,XREAL_1:139; A38: h"B is open & I[01]=TopSpaceMetr(Closed-Interval-MSpace(0,1)) by A8,A19 ,TOPMETR:20,def 6,def 7,UNIFORM1:2; h.s8=pro1.(f.s8) by A20,A30,BORSUK_1:40,FUNCT_1:12 .=proj1.p8 by A29,A31,FUNCT_1:49 .=p8`1 by PSCOMP_1:def 5; then s8 in h"B by A20,A30,A37,BORSUK_1:40,FUNCT_1:def 7; then consider r0 being Real such that A39: r0>0 and A40: Ball(s8m,r0) c= h"B by A38,TOPMETR:15; reconsider r0 as Real; reconsider r01=min(s8-s2,r0) as Real; the carrier of Closed-Interval-MSpace(0,1)=[.0,1.] & Ball(s8n,r01 )= (].s8- r01,s8+r01 .[) by FRECHET:7,TOPMETR:10; then A41: Ball(s8m,r01)= (].s8-r01,s8+r01 .[) /\ [.0,1.] by TOPMETR:9; s8>s2 by A4,A11,A31,A33,A36,XXREAL_0:1; then s8-s2>0 by XREAL_1:50; then A42: r01>0 by A39,XXREAL_0:21; then A43: r01-r01/2+r01/2>0+r01/2 by XREAL_1:6; then A44: s8-r01 0 by A42,XREAL_1:139; then A46: s8+-(r01/2) s8-r01 by A43,XREAL_1:10; Ball(s8m,r01) c= Ball(s8m,r0) by PCOMPS_1:1,XXREAL_0:17; then A49: (].s8-r01,s8+r01 .[)/\ [.0,1.] c= h"B by A40,A41; reconsider s70=s8-r01/2 as Real; s8-s2>=r01 by XXREAL_0:17; then -(s8-s2)<= -r01 by XREAL_1:24; then A50: s2-s8+s8<= -r01+s8 by XREAL_1:7; --(r01/2)> 0 by A42,XREAL_1:139; then -(r01/2) < 0; then A51: s8+0>s8+-r01/2 by XREAL_1:8; then A52: 1>=s70 by A32,XXREAL_0:2; 1-0>s8-r01/2 by A32,A45,XREAL_1:15; then s8-r01/2 in [.0,1.] by A22,A50,A48,XXREAL_1:1; then A53: s8-r01/2 in (].s8-r01,s8+r01 .[)/\ [.0,1.] by A47,XBOOLE_0:def 4; then A54: h.(s8-r01/2) in B by A49,FUNCT_1:def 7; A55: s8-r01/2 in dom h by A49,A53,FUNCT_1:def 7; A56: for p7 being Point of TOP-REAL 2 st p7=f.s70 holds p7`1<>e proof let p7 be Point of TOP-REAL 2; assume A57: p7=f.s70; s70 in [.0,1.] by A22,A50,A44,A52,XXREAL_1:1; then A58: p7 in rng f by A12,A57,BORSUK_1:40,FUNCT_1:def 3; A59: rng f=[#]((TOP-REAL 2)|P) by A5,TOPS_2:def 5 .=P by PRE_TOPC:def 5; A60: h.s70=pro1.(f.s70) by A55,FUNCT_1:12 .=pr1a.(p7) by A57,A58,A59,FUNCT_1:49 .=p7`1 by PSCOMP_1:def 5; then A61: p7`1 =0; then p8`1-(p8`1-e)/2 =0/2 by A64; hence contradiction by A65; end; case A66: p8`1-e<0; then e< p8`1+(-(p8`1-e))/2 by A61,A63,ABSVALUE:def 1; then p8`1/2+e/2>e/2+e/2; then p8`1/2>e/2 by XREAL_1:7; then A67: p8`1/2-e/2>e/2-e/2 by XREAL_1:14; (p8`1-e)/2<=0/2 by A66; hence contradiction by A67; end; end; hence contradiction; end; hence thesis; end; s70>=s2 by A50,A44,XXREAL_0:2; then consider s7 being Real such that A68: s8>s7 and A69: 1>=s7 & s7>=s2 & for p7 being Point of TOP-REAL 2 st p7=f.s7 holds p7`1 <>e by A51,A52,A56; s7 in R by A69; then s7 >=s0 by A21,SEQ_4:def 2; hence contradiction by A34,A68,XXREAL_0:2; end; hence thesis; end; assume not p is_OSout P,p1,p2,e; then consider p4 being Point of TOP-REAL 2 such that A70: LE p9,p4,P,p1,p2 and A71: p4<>p9 and A72: (for p5 being Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE p9,p5 , P,p1,p2 holds p5`1<=e)or for p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p9,p6,P,p1,p2 holds p6`1>=e by A1,A3,A4,A24,A26; A73: p9 in P by A70,JORDAN5C:def 3; now per cases by A72; case A74: for p5 being Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE p9 ,p5,P,p1,p2 holds p5`1<=e; A75: now p4 in P by A70,JORDAN5C:def 3; then p4 in rng f by A9,PRE_TOPC:def 5; then consider xs4 being object such that A76: xs4 in dom f and A77: p4=f.xs4 by FUNCT_1:def 3; reconsider s4=xs4 as Real by A76; A78: s4<=1 by A76,BORSUK_1:40,XXREAL_1:1; assume A79: not ex p51 being Point of TOP-REAL 2 st LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 & p51`1 =e & p51`1<=e by A74,A79; hence thesis by XXREAL_0:1; end; A81: now assume s4>s0; then --(s4-s0)>0 by XREAL_1:50; then -(s4-s0)<0; then A82: (s0-s4)/2<0 by XREAL_1:141; then -((s0-s4)/2)>0 by XREAL_1:58; then consider r being Real such that A83: r in R and A84: r =s7 & s7>=s2 & for q being Point of TOP-REAL 2 st q=f.s7 holds q`1<>e by A83; then r in [.0,1.] by A22,XXREAL_1:1; then f.rss in rng f by A12,BORSUK_1:40,FUNCT_1:def 3; then f.rss in P by A9,PRE_TOPC:def 5; then reconsider pss=f.rss as Point of TOP-REAL 2; s4+0>s4+(s0-s4)/2 by A82,XREAL_1:8; then A86: s4>r by A84,XXREAL_0:2; then A87: 1>r by A78,XXREAL_0:2; A88: r>=s0 by A21,A83,SEQ_4:def 2; then A89: LE p9,pss,P,p1,p2 by A1,A5,A6,A7,A22,A23,A18,A87,JORDAN5C:8; LE pss,p4,P,p1,p2 by A1,A5,A6,A7,A22,A18,A77,A78,A88,A86,A87, JORDAN5C:8; then pss`1=e by A80,A89; hence contradiction by A85; end; 0<=s4 by A76,BORSUK_1:40,XXREAL_1:1; then s4>=s0 by A5,A6,A7,A23,A70,A77,A78,JORDAN5C:def 3; hence contradiction by A71,A77,A81,XXREAL_0:1; end; now assume ex p51 being Point of TOP-REAL 2 st LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 & p51`1 =e; A100: now p4 in P by A70,JORDAN5C:def 3; then p4 in rng f by A9,PRE_TOPC:def 5; then consider xs4 being object such that A101: xs4 in dom f and A102: p4=f.xs4 by FUNCT_1:def 3; reconsider s4=xs4 as Real by A101; A103: s4<=1 by A101,BORSUK_1:40,XXREAL_1:1; assume A104: not ex p51 being Point of TOP-REAL 2 st LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 & p51`1>e; A105: for p51 being Point of TOP-REAL 2 st LE p51,p4,P,p1,p2 & LE p9 ,p51,P,p1,p2 holds p51`1=e proof let p51 be Point of TOP-REAL 2; assume LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2; then p51`1<=e & p51`1>=e by A99,A104; hence thesis by XXREAL_0:1; end; A106: now assume s4>s0; then --(s4-s0)>0 by XREAL_1:50; then -(s4-s0)<0; then A107: (s0-s4)/2<0 by XREAL_1:141; then -((s0-s4)/2)>0 by XREAL_1:58; then consider r being Real such that A108: r in R and A109: r =s7 & s7>=s2 & for q being Point of TOP-REAL 2 st q=f.s7 holds q`1<>e by A108; then r in [.0,1.] by A22,XXREAL_1:1; then f.rss in rng f by A12,BORSUK_1:40,FUNCT_1:def 3; then f.rss in P by A9,PRE_TOPC:def 5; then reconsider pss=f.rss as Point of TOP-REAL 2; s4+0>s4+(s0-s4)/2 by A107,XREAL_1:8; then A111: s4>r by A109,XXREAL_0:2; then A112: 1>r by A103,XXREAL_0:2; A113: r>=s0 by A21,A108,SEQ_4:def 2; then A114: LE p9,pss,P,p1,p2 by A1,A5,A6,A7,A22,A23,A18,A112,JORDAN5C:8; LE pss,p4,P,p1,p2 by A1,A5,A6,A7,A22,A18,A102,A103,A113,A111,A112, JORDAN5C:8; then pss`1=e by A105,A114; hence contradiction by A110; end; 0<=s4 by A101,BORSUK_1:40,XXREAL_1:1; then s4>=s0 by A5,A6,A7,A23,A70,A102,A103,JORDAN5C:def 3; hence contradiction by A71,A102,A106,XXREAL_0:1; end; now assume ex p51 being Point of TOP-REAL 2 st LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 & p51`1>e; then consider p51 being Point of TOP-REAL 2 such that A115: LE p51,p4,P,p1,p2 and A116: LE p9,p51,P,p1,p2 and A117: p51`1>e; A118: for p5 being Point of TOP-REAL 2 st LE p5,p51,P,p1,p2 & LE p, p5,P,p1,p2 holds p5`1>=e proof let p5 be Point of TOP-REAL 2; assume that A119: LE p5,p51,P,p1,p2 and A120: LE p,p5,P,p1,p2; A121: LE p5,p4,P,p1,p2 by A115,A119,JORDAN5C:13; A122: p5 in P by A119,JORDAN5C:def 3; then A123: p5=p9 implies LE p9,p5,P,p1,p2 by JORDAN5C:9; now per cases by A1,A73,A122,A123,JORDAN5C:14; case LE p9,p5,P,p1,p2; hence thesis by A99,A121; end; case LE p5,p9,P,p1,p2; hence thesis by A26,A120; end; end; hence thesis; end; LE p,p51,P,p1,p2 by A24,A116,JORDAN5C:13; hence p is_Rout P,p1,p2,e by A1,A3,A4,A117,A118; end; hence p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e by A100; end; end; hence p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e; end; hence thesis; end; theorem Th11: for P being Subset of I[01],s being Real st P=[.0,s.[ holds P is open proof A1: [#]I[01]=[.0,1.] by TOPMETR:18,20; let P be Subset of I[01],s be Real; assume A2: P=[.0,s.[; per cases; suppose A3: s in [.0,1.]; reconsider T=[.0,1.] as Subset of R^1 by TOPMETR:17; 0 in [.0,1.] by XXREAL_1:1; then [.0,s.[ c= [.0,s.] & [.0,s.] c= [.0,1.] by A3,XXREAL_1:24 ,XXREAL_2:def 12; then [.0,s.[ c= [.0,1.]; then P c= [#](R^1|T) by A2,PRE_TOPC:def 5; then reconsider P2=P as Subset of R^1|T; reconsider Q=].-1,s.[ as Subset of R^1 by TOPMETR:17; A4: s<=1 by A3,XXREAL_1:1; A5: [.0,s.[ c= ].-1,s.[ /\ [.0,1.] proof let x be object; assume A6: x in [.0,s.[; then reconsider sx=x as Real; A7: 0<=sx by A6,XXREAL_1:3; A8: sx ~~1; A15: for r being Real st 0<=r & r~~~~sx by XXREAL_0:2; then A9: x in ].s,2.[ by A7,XXREAL_1:4; x in [.0,1.] by A4,A7,A8,XXREAL_1:1; hence thesis by A9,XBOOLE_0:def 4; end; ].s,2.[ /\ [.0,1.] c= ].s,1.] proof let x be object; assume A10: x in ].s,2.[ /\ [.0,1.]; then reconsider sx=x as Real; x in [.0,1.] by A10,XBOOLE_0:def 4; then A11: sx<=1 by XXREAL_1:1; x in ].s,2.[ by A10,XBOOLE_0:def 4; then s~~1; then ].s,1.] ={} by XXREAL_1:26; then P in the topology of I[01] by A2,PRE_TOPC:1; hence thesis by PRE_TOPC:def 2; end; case A14: s<0; A15: for r being Real st s =0 proof let r be Real; assume s =0 & P1= {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st s =0 and A2: P1= {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st s {}; theorem Th15: for P being non empty Subset of TOP-REAL 2, P1 being Subset of ( TOP-REAL 2)|P, f being Function of I[01],(TOP-REAL 2)|P, s being Real st s<=1 & f is being_homeomorphism & P1= {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st 0<=ss & ss ~~=0 & f is being_homeomorphism & P1= {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st s~~=0 and A2: f is being_homeomorphism and A3: P1= {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st s {} & Q is open by Th12; A7: f" is being_homeomorphism by A2,TOPS_2:56; then A8: f" is one-to-one by TOPS_2:def 5; rng (f") =[#](I[01]) by A7,TOPS_2:def 5; then f" is onto by FUNCT_2:def 3; then (f")"=(f" qua Function)" by A8,TOPS_2:def 4; then A9: ((f")").:Q=(f")"Q by A8,FUNCT_1:85; P1=f.:Q & f" is continuous by A1,A2,A3,Th14,TOPS_2:def 5; hence thesis by A6,A4,A9,TOPS_2:43; end; theorem Th17: for T being non empty TopStruct, Q1,Q2 being Subset of T, p1,p2 being Point of T st Q1 /\ Q2={} & Q1 \/ Q2=the carrier of T & p1 in Q1 & p2 in Q2 & Q1 is open & Q2 is open holds not ex P being Function of I[01],T st P is continuous & P.0=p1 & P.1=p2 proof let T be non empty TopStruct, Q1,Q2 be Subset of T, p1,p2 be Point of T; assume that A1: Q1 /\ Q2={} and A2: Q1 \/ Q2=the carrier of T and A3: p1 in Q1 and A4: p2 in Q2 and A5: Q1 is open & Q2 is open; assume ex P being Function of I[01],T st P is continuous & P.0=p1 & P.1=p2; then consider P being Function of I[01],T such that A6: P is continuous and A7: P.0=p1 and A8: P.1=p2; [#]T <> {}; then A9: P"Q1 is open & P"Q2 is open by A5,A6,TOPS_2:43; A10: [#]I[01]=[.0,1.] by TOPMETR:18,20; then 0 in the carrier of I[01] by XXREAL_1:1; then 0 in dom P by FUNCT_2:def 1; then A11: [#]I[01]=the carrier of I[01] & P"Q1 <> {}I[01] by A3,A7,FUNCT_1:def 7; P"Q1 /\ P"Q2 =P"(Q1 /\ Q2) by FUNCT_1:68 .={} by A1; then A12: not P"Q1 meets P"Q2 by XBOOLE_0:def 7; 1 in the carrier of I[01] by A10,XXREAL_1:1; then 1 in dom P by FUNCT_2:def 1; then A13: P"Q2 <> {}I[01] by A4,A8,FUNCT_1:def 7; P"Q1 \/ P"Q2 =P"(Q1 \/ Q2) by RELAT_1:140 .= the carrier of I[01] by A2,FUNCT_2:40; hence contradiction by A9,A11,A13,A12,CONNSP_1:11,TREAL_1:19; end; theorem Th18: for P being non empty Subset of TOP-REAL 2, Q being Subset of ( TOP-REAL 2)|P, p1,p2,q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & q in P & q<>p1 & q<>p2 & Q=P\{q} holds not Q is connected & not ex R being Function of I[01],((TOP-REAL 2)|P)|Q st R is continuous & R.0=p1 & R.1=p2 proof let P be non empty Subset of TOP-REAL 2, Q be Subset of (TOP-REAL 2)|P, p1, p2,q be Point of TOP-REAL 2; assume that A1: P is_an_arc_of p1,p2 and A2: q in P and A3: q<>p1 and A4: q<>p2 and A5: Q=P\{q}; consider f being Function of I[01], (TOP-REAL 2)|P such that A6: f is being_homeomorphism and A7: f.0 = p1 and A8: f.1 = p2 by A1,TOPREAL1:def 1; A9: rng f=[#]((TOP-REAL 2)|P) by A6,TOPS_2:def 5; A10: [#]I[01]=[.0,1.] by TOPMETR:18,20; A11: [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 5; then consider xs being object such that A12: xs in dom f and A13: f.xs=q by A2,A9,FUNCT_1:def 3; A14: dom f=[#]I[01] by A6,TOPS_2:def 5; reconsider s=xs as Real by A12; {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st s 0 by A12,A10,A17,XXREAL_1:1; then ss in dom f by A14,A10,A18,XXREAL_1:1; then q0 in rng f by A19,FUNCT_1:def 3; hence thesis by A15; end; then reconsider P29= {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st s< ss & ss<=1 & q0=f.ss} as Subset of (TOP-REAL 2)|P; A20: 0<=s by A12,A10,XXREAL_1:1; then A21: P29 is open by A6,Th16; A22: P29 c= Q proof let x be object; assume x in P29; then consider q00 being Point of TOP-REAL 2 such that A23: q00=x and A24: ex ss being Real st s 0 by A12,A10,A25,XXREAL_1:1; then A28: ss in dom f by A14,A10,A26,XXREAL_1:1; now assume A29: q00=q; f is one-to-one by A6,TOPS_2:def 5; hence contradiction by A12,A13,A25,A27,A28,A29,FUNCT_1:def 4; end; then A30: not q00 in {q} by TARSKI:def 1; q00 in P by A9,A11,A27,A28,FUNCT_1:def 3; hence thesis by A5,A23,A30,XBOOLE_0:def 5; end; {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st 0<=ss & ss ~~=s; then t>s by A13,A41,A43,XXREAL_0:1; then ex ss being Real st s~~0 by A12,A10,A56,XXREAL_1:1; then A59: ss2 in dom f by A14,A10,A57,XXREAL_1:1; f is one-to-one by A6,TOPS_2:def 5; hence contradiction by A48,A51,A52,A54,A56,A58,A53,A59,FUNCT_1:def 4; end; 1>s by A4,A8,A13,A36,XXREAL_0:1; then A60: p2 in {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st s {} by A60,A22,XBOOLE_1:28; then A62: P29 meets Q by XBOOLE_0:def 7; A63: P19 c= Q proof let x be object; assume x in P19; then consider q00 being Point of TOP-REAL 2 such that A64: q00=x and A65: ex ss being Real st 0<=ss & ss ~~0 by A3,A7,A13; then A73: p1 in {q0 where q0 is Point of TOP-REAL 2: ex ss being Real st 0<=ss & ss~~~~{} by A63,XBOOLE_1:28; then P19 meets Q by XBOOLE_0:def 7; hence not Q is connected by A37,A21,A38,A62,A45,TOPREAL5:1; the carrier of T =Q by A61,PRE_TOPC:def 5; then A74: P199 \/ P299 = the carrier of ((TOP-REAL 2)|P)|Q by A38,XBOOLE_0:def 10; P299=P29 /\ (the carrier of T) by XBOOLE_1:28; then A75: P299 is open by A21,A61,TOPS_2:24; P199 /\ P299={} by A45,XBOOLE_0:def 7; hence thesis by A73,A60,A72,A75,A74,Th17; end; theorem Th19: for P being non empty 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 LE q1,q2, P,p1,p2 or LE q2,q1,P,p1,p2 proof let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2; assume that A1: P is_an_arc_of p1,p2 and A2: q1 in P and A3: q2 in P; per cases; suppose q1<>q2; hence thesis by A1,A2,A3,JORDAN5C:14; end; suppose q1=q2; hence thesis by A2,JORDAN5C:9; end; end; theorem Th20: :: Another version of TOPMETR3:18 for n being Nat,p1,p2 being Point of TOP-REAL n, P,P1 being non empty Subset of TOP-REAL n st P is_an_arc_of p1,p2 & P1 is_an_arc_of p1,p2 & P1 c= P holds P1=P proof let n be Nat,p1,p2 be Point of TOP-REAL n, P,P1 be non empty Subset of TOP-REAL n; assume that A1: P is_an_arc_of p1,p2 and A2: P1 is_an_arc_of p1,p2 and A3: P1 c= P; P1 is_an_arc_of p2,p1 by A2,JORDAN5B:14; hence thesis by A1,A3,TOPMETR3:14; end; theorem Th21: for P being non empty 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 & p2<>q1 holds Segment(P,p1,p2, q1,p2) is_an_arc_of q1,p2 proof let P be non empty Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2; assume that A1: P is_an_arc_of p1,p2 and A2: q1 in P and A3: p2<>q1; LE q1,p2,P,p1,p2 by A1,A2,JORDAN5C:10; hence thesis by A1,A3,JORDAN16:21; end; theorem Th22: for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,q3 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q3,P,p1, p2 holds Segment(P,p1,p2,q1,q2) \/ Segment(P,p1,p2,q2,q3) =Segment(P,p1,p2,q1, q3) proof let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2,q3 be Point of TOP-REAL 2; assume that A1: P is_an_arc_of p1,p2 and A2: LE q1,q2,P,p1,p2 and A3: LE q2,q3,P,p1,p2; A4: q2 in P by A2,JORDAN5C:def 3; A5: Segment(P,p1,p2,q1,q3) c= Segment(P,p1,p2,q1,q2) \/ Segment(P,p1,p2,q2, q3) proof let x be object; assume x in Segment(P,p1,p2,q1,q3); then x in {p3 where p3 is Point of TOP-REAL 2: LE q1,p3,P,p1,p2 & LE p3,q3 ,P,p1,p2} by JORDAN6:26; then consider p3 being Point of TOP-REAL 2 such that A6: x=p3 and A7: LE q1,p3,P,p1,p2 and A8: LE p3,q3,P,p1,p2; A9: p3 in P by A7,JORDAN5C:def 3; now per cases; suppose A10: p3=q2; then LE p3,q2,P,p1,p2 by A4,JORDAN5C:9; then x in {p31 where p31 is Point of TOP-REAL 2: LE q1,p31,P,p1,p2 & LE p31,q2,P,p1,p2} by A2,A6,A10; hence x in Segment(P,p1,p2,q1,q2) or x in Segment(P,p1,p2,q2,q3) by JORDAN6:26; end; suppose A11: p3<>q2; now per cases by A1,A4,A9,A11,JORDAN5C:14; case LE p3,q2,P,p1,p2 & not LE q2,p3,P,p1,p2; then x in {p31 where p31 is Point of TOP-REAL 2: LE q1,p31,P,p1,p2 & LE p31,q2,P,p1,p2} by A6,A7; hence x in Segment(P,p1,p2,q1,q2) or x in Segment(P,p1,p2,q2,q3) by JORDAN6:26; end; case LE q2,p3,P,p1,p2 & not LE p3,q2,P,p1,p2; then x in {p31 where p31 is Point of TOP-REAL 2: LE q2,p31,P,p1,p2 & LE p31,q3,P,p1,p2} by A6,A8; hence x in Segment(P,p1,p2,q1,q2) or x in Segment(P,p1,p2,q2,q3) by JORDAN6:26; end; end; hence x in Segment(P,p1,p2,q1,q2) or x in Segment(P,p1,p2,q2,q3); end; end; hence thesis by XBOOLE_0:def 3; end; Segment(P,p1,p2,q1,q2) \/ Segment(P,p1,p2,q2,q3) c= Segment(P,p1,p2,q1, q3) proof let x be object; assume A12: x in Segment(P,p1,p2,q1,q2) \/ Segment(P,p1,p2,q2,q3); per cases by A12,XBOOLE_0:def 3; suppose x in Segment(P,p1,p2,q1,q2); then x in {p where p is Point of TOP-REAL 2: LE q1,p,P,p1,p2 & LE p,q2,P, p1,p2} by JORDAN6:26; then consider p being Point of TOP-REAL 2 such that A13: x=p & LE q1,p,P,p1,p2 and A14: LE p,q2,P,p1,p2; LE p,q3,P,p1,p2 by A3,A14,JORDAN5C:13; then x in {p3 where p3 is Point of TOP-REAL 2: LE q1,p3,P,p1,p2 & LE p3, q3,P,p1,p2} by A13; hence thesis by JORDAN6:26; end; suppose x in Segment(P,p1,p2,q2,q3); then x in {p where p is Point of TOP-REAL 2: LE q2,p,P,p1,p2 & LE p,q3,P ,p1,p2} by JORDAN6:26; then consider p being Point of TOP-REAL 2 such that A15: x=p and A16: LE q2,p,P,p1,p2 and A17: LE p,q3,P,p1,p2; LE q1,p,P,p1,p2 by A2,A16,JORDAN5C:13; then x in {p3 where p3 is Point of TOP-REAL 2: LE q1,p3,P,p1,p2 & LE p3, q3,P,p1,p2} by A15,A17; hence thesis by JORDAN6:26; end; end; hence thesis by A5,XBOOLE_0:def 10; end; theorem for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,q3 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds Segment(P,p1,p2,q1,q2) /\ Segment(P,p1,p2,q2,q3) = {q2} proof let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2,q3 be Point of TOP-REAL 2; assume that A1: P is_an_arc_of p1,p2 and A2: LE q1,q2,P,p1,p2 and A3: LE q2,q3,P,p1,p2; A4: q2 in P by A2,JORDAN5C:def 3; A5: {q2} c= Segment(P,p1,p2,q1,q2) /\ Segment(P,p1,p2,q2,q3) proof set p3=q2; let x be object; assume x in {q2}; then A6: x=q2 by TARSKI:def 1; LE q2,p3,P,p1,p2 by A4,JORDAN5C:9; then x in {p31 where p31 is Point of TOP-REAL 2: LE q2,p31,P,p1,p2 & LE p31,q3,P,p1,p2} by A3,A6; then A7: x in Segment(P,p1,p2,q2,q3) by JORDAN6:26; LE p3,q2,P,p1,p2 by A4,JORDAN5C:9; then x in {p31 where p31 is Point of TOP-REAL 2: LE q1,p31,P,p1,p2 & LE p31,q2,P,p1,p2} by A2,A6; then x in Segment(P,p1,p2,q1,q2) by JORDAN6:26; hence thesis by A7,XBOOLE_0:def 4; end; Segment(P,p1,p2,q1,q2) /\ Segment(P,p1,p2,q2,q3) c= {q2} proof let x be object; assume A8: x in Segment(P,p1,p2,q1,q2) /\ Segment(P,p1,p2,q2,q3); then x in Segment(P,p1,p2,q2,q3) by XBOOLE_0:def 4; then x in {p4 where p4 is Point of TOP-REAL 2: LE q2,p4,P,p1,p2 & LE p4,q3 ,P,p1,p2} by JORDAN6:26; then A9: ex p4 being Point of TOP-REAL 2 st x=p4 & LE q2,p4,P,p1, p2 & LE p4,q3 ,P,p1,p2; x in Segment(P,p1,p2,q1,q2) by A8,XBOOLE_0:def 4; then x in {p where p is Point of TOP-REAL 2: LE q1,p,P,p1,p2 & LE p,q2,P,p1 ,p2} by JORDAN6:26; then ex p being Point of TOP-REAL 2 st x=p & LE q1,p,P,p1,p2 & LE p,q2,P,p1 ,p2; then x=q2 by A1,A9,JORDAN5C:12; hence thesis by TARSKI:def 1; end; hence thesis by A5,XBOOLE_0:def 10; end; theorem Th24: 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 Segment(P,p1,p2,p1,p2)=P proof let P be non empty Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; assume P is_an_arc_of p1,p2; then A1: R_Segment(P,p1,p2,p1)=P & L_Segment(P,p1,p2,p2)=P by JORDAN6:22,24; R_Segment(P,p1,p2,p1) /\ L_Segment(P,p1,p2,p2)=Segment(P,p1,p2,p1,p2) by JORDAN6:def 5; hence thesis by A1; end; theorem Th25: for P,Q1 being non empty Subset of TOP-REAL 2, p1,p2,q1,q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & Q1 is_an_arc_of q1,q2 & LE q1,q2, P,p1,p2 & Q1 c= P holds Q1= Segment(P,p1,p2,q1,q2) proof let P,Q1 be non empty Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2; assume that A1: P is_an_arc_of p1,p2 and A2: Q1 is_an_arc_of q1,q2 and A3: LE q1,q2,P,p1,p2 and A4: Q1 c= P; reconsider Q0=Segment(P,p1,p2,q1,q2) as non empty Subset of TOP-REAL 2 by A3, JORDAN16:18; A5: q1<>q2 by A2,JORDAN6:37; then A6: Segment(P,p1,p2,q1,q2) is_an_arc_of q1,q2 by A1,A3,JORDAN16:21; A7: q2 in P by A3,JORDAN5C:def 3; A8: now assume A9: q1=p2; LE q2,p2,P,p1,p2 by A1,A7,JORDAN5C:10; hence contradiction by A1,A2,A3,A9,JORDAN5C:12,JORDAN6:37; end; A10: q1 in P by A3,JORDAN5C:def 3; A11: now assume A12: q2=p1; LE p1,q1,P,p1,p2 by A1,A10,JORDAN5C:10; hence contradiction by A1,A2,A3,A12,JORDAN5C:12,JORDAN6:37; end; A13: p1 in P & p2 in P by A1,TOPREAL1:1; now A14: LE p1,q1,P,p1,p2 by A1,A10,JORDAN5C:10; then A15: Segment(P,p1,p2,p1,q1)\/ Segment(P,p1,p2,q1,q2) =Segment(P,p1,p2,p1, q2) by A1,A3,Th22; A16: [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 5; A17: LE q2,p2,P,p1,p2 by A1,A7,JORDAN5C:10; A18: [#]I[01]=the carrier of I[01]; Q0 is_an_arc_of q1,q2 by A1,A3,A5,JORDAN16:21; then A19: q2 in Q0 by TOPREAL1:1; assume not Q1 c= Q0; then consider x8 being object such that A20: x8 in Q1 and A21: not x8 in Q0; reconsider q=x8 as Point of TOP-REAL 2 by A20; A22: q<>q1 by A3,A21,JORDAN16:5; LE p1,q2,P,p1,p2 by A3,A14,JORDAN5C:13; then Segment(P,p1,p2,p1,q2)\/Segment(P,p1,p2,q2,p2)=Segment(P,p1,p2,p1,p2 ) by A1,A17,Th22 .=P by A1,Th24; then A23: q in Segment(P,p1,p2,p1,q2) or q in Segment(P,p1,p2,q2,p2) by A4,A20, XBOOLE_0:def 3; now per cases by A21,A15,A23,XBOOLE_0:def 3; case A24: q in Segment(P,p1,p2,p1,q1); A25: not q in {q1} by A22,TARSKI:def 1; not q2 in {q1} by A5,TARSKI:def 1; then reconsider Qa=P\{q1} as non empty Subset of (TOP-REAL 2)|P by A7,A16, XBOOLE_0:def 5,XBOOLE_1:36; A26: the carrier of ((TOP-REAL 2)|P)|Qa=Qa by PRE_TOPC:8; reconsider Qa9=Qa as Subset of TOP-REAL 2; A27: the carrier of ((TOP-REAL 2)|P)|Qa=Qa by PRE_TOPC:8; A28: Segment(Q1,q1,q2,q,q2) is_an_arc_of q,q2 by A2,A20,A21,A19,Th21; then consider f2 being Function of I[01],(TOP-REAL 2)|Segment(Q1,q1,q2,q,q2 ) such that A29: f2 is being_homeomorphism and A30: f2.0=q & f2.1=q2 by TOPREAL1:def 1; A31: rng f2=[#]((TOP-REAL 2)|Segment(Q1,q1,q2,q,q2)) by A29,TOPS_2:def 5 .=Segment(Q1,q1,q2,q,q2) by PRE_TOPC:def 5; A32: ( not p2 in {q1})& not q2 in {q1} by A5,A8,TARSKI:def 1; q in {p3 where p3 is Point of TOP-REAL 2: LE p1,p3,P,p1,p2 & LE p3,q1,P,p1,p2} by A24,JORDAN6:26; then A33: ex p3 being Point of TOP-REAL 2 st q=p3 & LE p1,p3,P,p1, p2 & LE p3,q1,P,p1,p2; A34: now assume A35: p1=q1; then q=p1 by A1,A33,JORDAN5C:12; hence contradiction by A6,A21,A35,TOPREAL1:1; end; then not p1 in {q1} by TARSKI:def 1; then reconsider p19=p1,q9=q,q29=q2,p29=p2 as Point of ((TOP-REAL 2)|P)|Qa by A4,A7,A13,A20,A26,A32,A25,XBOOLE_0:def 5; now per cases; case q<>p1; then A36: Segment(P,p1,p2,p1,q) is_an_arc_of p1,q by A1,A4,A20,JORDAN16:24; then consider f1 being Function of I[01],(TOP-REAL 2)|Segment(P,p1,p2, p1,q) such that A37: f1 is being_homeomorphism and A38: f1.0=p1 & f1.1=q by TOPREAL1:def 1; A39: rng f1=[#]((TOP-REAL 2)|Segment(P,p1,p2,p1,q)) by A37,TOPS_2:def 5 .=Segment(P,p1,p2,p1,q) by PRE_TOPC:def 5; {p where p is Point of TOP-REAL 2: LE p1,p,P,p1,p2 & LE p,q,P ,p1, p2 } c= Qa proof let x be object; assume x in {p where p is Point of TOP-REAL 2: LE p1,p,P,p1,p2 & LE p,q,P,p1,p2}; then A40: ex p being Point of TOP-REAL 2 st x=p & LE p1,p,P,p1,p2 & LE p,q,P,p1,p2; then x<>q1 by A1,A22,A33,JORDAN5C:12; then A41: not x in {q1} by TARSKI:def 1; x in P by A40,JORDAN5C:def 3; hence thesis by A41,XBOOLE_0:def 5; end; then A42: Segment(P,p1,p2,p1,q) c= Qa by JORDAN6:26; dom f1=the carrier of I[01] by A18,A37,TOPS_2:def 5; then reconsider g1=f1 as Function of I[01],((TOP-REAL 2)|P)|Qa by A26,A39,A42, FUNCT_2:2; A43: f1 is continuous by A37,TOPS_2:def 5; A44: for G being Subset of ((TOP-REAL 2)|P)|Qa st G is open holds g1"G is open proof let G be Subset of ((TOP-REAL 2)|P)|Qa; A45: ((TOP-REAL 2)|P)|Qa=(TOP-REAL 2)|Qa9 by PRE_TOPC:7,XBOOLE_1:36; assume G is open; then consider G4 being Subset of (TOP-REAL 2) such that A46: G4 is open and A47: G=G4 /\ [#]((TOP-REAL 2)|Qa9) by A45,TOPS_2:24; reconsider G5=G4 /\ [#]((TOP-REAL 2)|Segment(P,p1,p2,p1,q)) as Subset of ((TOP-REAL 2)|Segment(P,p1,p2,p1,q)); A48: G5 is open by A46,TOPS_2:24; A49: rng g1=[#]((TOP-REAL 2)|Segment(P,p1,p2,p1,q)) by A37, TOPS_2:def 5 .= Segment(P,p1,p2,p1,q) by PRE_TOPC:def 5; A50: p1 in Segment(P,p1,p2,p1,q) by A36,TOPREAL1:1; A51: f1"G5=g1"(G4 /\ Segment(P,p1,p2,p1,q)) by PRE_TOPC:def 5 .=g1"(G4) /\ g1"(Segment(P,p1,p2,p1,q)) by FUNCT_1:68; g1"G=g1"G4 /\ g1"([#]((TOP-REAL 2)|Qa9)) by A47,FUNCT_1:68 .=g1"G4 /\ g1"Qa9 by PRE_TOPC:def 5 .=g1"G4 /\ g1"((rng g1) /\ Qa9) by RELAT_1:133 .=g1"G4 /\ g1"(Segment(P,p1,p2,p1,q)) by A42,A49,XBOOLE_1:28; hence thesis by A43,A50,A48,A51,TOPS_2:43; end; [#](((TOP-REAL 2)|P)|Qa) <> {}; then A52: g1 is continuous by A44,TOPS_2:43; then p19,q9 are_connected by A38,BORSUK_2:def 1; then g1 is Path of p19,q9 by A38,A52,BORSUK_2:def 2; hence ex G1 being Path of p19,q9 st G1 is continuous & G1.0=p19 & G1.1=q9 by A38,A52; end; case A53: q=p1; consider g01 being Function of I[01],(((TOP-REAL 2)|P)|Qa) such that A54: g01 is continuous & g01.0=p19 & g01.1=p19 by BORSUK_2:3; p19,p19 are_connected; then g01 is Path of p19,p19 by A54,BORSUK_2:def 2; hence ex G1 being Path of p19,q9 st G1 is continuous & G1.0=p19 & G1.1=q9 by A53,A54; end; end; then consider G1 being Path of p19,q9 such that A55: G1 is continuous & G1.0=p19 & G1.1=q9; now per cases; case q2<>p2; then A56: Segment(P,p1,p2,q2,p2) is_an_arc_of q2,p2 by A1,A7,Th21; then consider f3 being Function of I[01],(TOP-REAL 2)|Segment(P,p1,p2, q2,p2) such that A57: f3 is being_homeomorphism and A58: f3.0=q2 & f3.1=p2 by TOPREAL1:def 1; A59: rng f3=[#]((TOP-REAL 2)|Segment(P,p1,p2,q2,p2)) by A57,TOPS_2:def 5 .=Segment(P,p1,p2,q2,p2) by PRE_TOPC:def 5; {p where p is Point of TOP-REAL 2: LE q2,p,P,p1,p2 & LE p,p2 ,P,p1, p2} c= Qa proof let x be object; assume x in {p where p is Point of TOP-REAL 2: LE q2,p,P,p1, p2 & LE p,p2,P,p1,p2}; then A60: ex p being Point of TOP-REAL 2 st x=p & LE q2,p,P,p1,p2 & LE p,p2,P,p1,p2; then x<>q1 by A1,A2,A3,JORDAN5C:12,JORDAN6:37; then A61: not x in {q1} by TARSKI:def 1; x in P by A60,JORDAN5C:def 3; hence thesis by A61,XBOOLE_0:def 5; end; then A62: Segment(P,p1,p2,q2,p2) c= Qa by JORDAN6:26; A63: the carrier of ((TOP-REAL 2)|P)|Qa=Qa by PRE_TOPC:8; dom f3=the carrier of I[01] by A18,A57,TOPS_2:def 5; then reconsider g3=f3 as Function of I[01],((TOP-REAL 2)|P)|Qa by A59,A63,A62,FUNCT_2:2; A64: f3 is continuous by A57,TOPS_2:def 5; A65: for G being Subset of ((TOP-REAL 2)|P)|Qa st G is open holds g3"G is open proof let G be Subset of ((TOP-REAL 2)|P)|Qa; A66: ((TOP-REAL 2)|P)|Qa=(TOP-REAL 2)|Qa9 by PRE_TOPC:7,XBOOLE_1:36; assume G is open; then consider G4 being Subset of (TOP-REAL 2) such that A67: G4 is open and A68: G=G4 /\ [#]((TOP-REAL 2)|Qa9) by A66,TOPS_2:24; reconsider G5=G4 /\ [#]((TOP-REAL 2)|Segment(P,p1,p2,q2,p2)) as Subset of ((TOP-REAL 2)|Segment(P,p1,p2,q2,p2)); A69: G5 is open by A67,TOPS_2:24; A70: rng g3=[#]((TOP-REAL 2)|Segment(P,p1,p2,q2,p2)) by A57, TOPS_2:def 5 .= Segment(P,p1,p2,q2,p2) by PRE_TOPC:def 5; A71: p2 in Segment(P,p1,p2,q2,p2) by A56,TOPREAL1:1; A72: f3"G5=g3"(G4 /\ Segment(P,p1,p2,q2,p2)) by PRE_TOPC:def 5 .=g3"(G4) /\ g3"(Segment(P,p1,p2,q2,p2)) by FUNCT_1:68; g3"G=g3"G4 /\ g3"([#]((TOP-REAL 2)|Qa9)) by A68,FUNCT_1:68 .=g3"G4 /\ g3"Qa9 by PRE_TOPC:def 5 .=g3"G4 /\ g3"((rng g3) /\ Qa9) by RELAT_1:133 .=g3"G4 /\ g3"(Segment(P,p1,p2,q2,p2)) by A62,A70,XBOOLE_1:28; hence thesis by A64,A71,A69,A72,TOPS_2:43; end; [#](((TOP-REAL 2)|P)|Qa) <> {}; then A73: g3 is continuous by A65,TOPS_2:43; then q29,p29 are_connected by A58,BORSUK_2:def 1; then g3 is Path of q29,p29 by A58,A73,BORSUK_2:def 2; hence ex G3 being Path of q29,p29 st G3 is continuous & G3.0=q29 & G3.1=p29 by A58,A73; end; case A74: q2=p2; consider g01 being Function of I[01],(((TOP-REAL 2)|P)|Qa) such that A75: g01 is continuous & g01.0=q29 & g01.1=q29 by BORSUK_2:3; q29,q29 are_connected; then g01 is Path of q29,q29 by A75,BORSUK_2:def 2; hence ex G3 being Path of q29,p29 st G3 is continuous & G3.0=q29 & G3.1=p29 by A74,A75; end; end; then consider G3 being Path of q29,p29 such that A76: G3 is continuous & G3.0=q29 & G3.1=p29; {p where p is Point of TOP-REAL 2: LE q,p,Q1,q1,q2 & LE p,q2,Q1, q1, q2} c= Qa proof let x be object; assume x in {p where p is Point of TOP-REAL 2: LE q,p,Q1,q1,q2 & LE p,q2,Q1,q1,q2}; then A77: ex p being Point of TOP-REAL 2 st x=p & LE q,p,Q1,q1,q2 & LE p, q2,Q1,q1,q2; now assume A78: x=q1; LE q1,q,Q1,q1,q2 by A2,A20,JORDAN5C:10; hence contradiction by A2,A22,A77,A78,JORDAN5C:12; end; then A79: not x in {q1} by TARSKI:def 1; x in Q1 by A77,JORDAN5C:def 3; hence thesis by A4,A79,XBOOLE_0:def 5; end; then A80: Segment(Q1,q1,q2,q,q2) c= Qa by JORDAN6:26; dom f2=the carrier of I[01] by A18,A29,TOPS_2:def 5; then reconsider g2=f2 as Function of I[01],((TOP-REAL 2)|P)|Qa by A31 ,A27,A80,FUNCT_2:2; A81: f2 is continuous by A29,TOPS_2:def 5; A82: for G being Subset of ((TOP-REAL 2)|P)|Qa st G is open holds g2"G is open proof let G be Subset of ((TOP-REAL 2)|P)|Qa; A83: ((TOP-REAL 2)|P)|Qa=(TOP-REAL 2)|Qa9 by PRE_TOPC:7,XBOOLE_1:36; assume G is open; then consider G4 being Subset of (TOP-REAL 2) such that A84: G4 is open and A85: G=G4 /\ [#]((TOP-REAL 2)|Qa9) by A83,TOPS_2:24; reconsider G5=G4 /\ [#]((TOP-REAL 2)|Segment(Q1,q1,q2,q,q2)) as Subset of ((TOP-REAL 2)|Segment(Q1,q1,q2,q,q2)); A86: G5 is open by A84,TOPS_2:24; A87: rng g2=[#]((TOP-REAL 2)|Segment(Q1,q1,q2,q,q2)) by A29,TOPS_2:def 5 .= Segment(Q1,q1,q2,q,q2) by PRE_TOPC:def 5; A88: q2 in Segment(Q1,q1,q2,q,q2) by A28,TOPREAL1:1; A89: f2"G5=g2"(G4 /\ Segment(Q1,q1,q2,q,q2)) by PRE_TOPC:def 5 .=g2"(G4) /\ g2"(Segment(Q1,q1,q2,q,q2)) by FUNCT_1:68; g2"G=g2"G4 /\ g2"([#]((TOP-REAL 2)|Qa9)) by A85,FUNCT_1:68 .=g2"G4 /\ g2"Qa9 by PRE_TOPC:def 5 .=g2"G4 /\ g2"((rng g2) /\ Qa9) by RELAT_1:133 .=g2"G4 /\ g2"(Segment(Q1,q1,q2,q,q2)) by A80,A87,XBOOLE_1:28; hence thesis by A81,A88,A86,A89,TOPS_2:43; end; [#](((TOP-REAL 2)|P)|Qa) <> {}; then A90: g2 is continuous by A82,TOPS_2:43; then q9,q29 are_connected by A30,BORSUK_2:def 1; then reconsider G2=g2 as Path of q9,q29 by A30,A90,BORSUK_2:def 2; A91: (G1+G2).1=q29 by A55,A30,A90,BORSUK_2:14; A92: (G1+G2) is continuous & (G1+G2).0=p19 by A55,A30,A90,BORSUK_2:14; then A93: ((G1+G2)+G3).1=p29 by A91,A76,BORSUK_2:14; (G1+G2)+G3 is continuous & ((G1+G2)+G3).0=p19 by A92,A91,A76, BORSUK_2:14; hence contradiction by A1,A10,A8,A34,A93,Th18; end; case A94: q in Segment(P,p1,p2,q2,p2); A95: ( not p1 in {q2})& not q1 in {q2} by A5,A11,TARSKI:def 1; not q1 in {q2} by A5,TARSKI:def 1; then reconsider Qa=P\{q2} as non empty Subset of (TOP-REAL 2)|P by A10,A16, XBOOLE_0:def 5,XBOOLE_1:36; A96: the carrier of ((TOP-REAL 2)|P)|Qa=Qa by PRE_TOPC:8; reconsider Qa9=Qa as Subset of TOP-REAL 2; A97: the carrier of ((TOP-REAL 2)|P)|Qa=Qa by PRE_TOPC:8; A98: Segment(Q1,q1,q2,q1,q) is_an_arc_of q1,q by A2,A20,A22,JORDAN16:24; then consider f2 being Function of I[01],(TOP-REAL 2)|Segment(Q1,q1,q2,q1,q ) such that A99: f2 is being_homeomorphism and A100: f2.0=q1 & f2.1=q by TOPREAL1:def 1; A101: rng f2=[#]((TOP-REAL 2)|Segment(Q1,q1,q2,q1,q)) by A99,TOPS_2:def 5 .=Segment(Q1,q1,q2,q1,q) by PRE_TOPC:def 5; A102: not q in {q2} by A21,A19,TARSKI:def 1; q in {p3 where p3 is Point of TOP-REAL 2: LE q2,p3,P,p1,p2 & LE p3,p2,P,p1,p2} by A94,JORDAN6:26; then A103: ex p3 being Point of TOP-REAL 2 st q=p3 & LE q2,p3,P,p1, p2 & LE p3,p2,P,p1,p2; A104: now assume A105: p2=q2; then q=p2 by A1,A103,JORDAN5C:12; hence contradiction by A6,A21,A105,TOPREAL1:1; end; then not p2 in {q2} by TARSKI:def 1; then reconsider p19=p1,q9=q,q19=q1,p29=p2 as Point of ((TOP-REAL 2)|P)|Qa by A4,A10,A13,A20,A96,A95,A102,XBOOLE_0:def 5; now per cases; case q<>p2; then A106: Segment(P,p1,p2,q,p2) is_an_arc_of q,p2 by A1,A4,A20,Th21; then consider f1 being Function of I[01],(TOP-REAL 2)|Segment(P,p1,p2,q ,p2) such that A107: f1 is being_homeomorphism and A108: f1.0=q & f1.1=p2 by TOPREAL1:def 1; A109: rng f1=[#]((TOP-REAL 2)|Segment(P,p1,p2,q,p2)) by A107,TOPS_2:def 5 .=Segment(P,p1,p2,q,p2) by PRE_TOPC:def 5; {p where p is Point of TOP-REAL 2: LE q,p,P,p1,p2 & LE p,p2, P,p1, p2} c= Qa proof let x be object; assume x in {p where p is Point of TOP-REAL 2: LE q,p,P,p1,p2 & LE p,p2,P,p1,p2}; then A110: ex p being Point of TOP-REAL 2 st x=p & LE q,p,P,p1,p2 & LE p,p2,P,p1,p2; then x<>q2 by A1,A21,A19,A103,JORDAN5C:12; then A111: not x in {q2} by TARSKI:def 1; x in P by A110,JORDAN5C:def 3; hence thesis by A111,XBOOLE_0:def 5; end; then A112: Segment(P,p1,p2,q,p2) c= Qa by JORDAN6:26; dom f1=the carrier of I[01] by A18,A107,TOPS_2:def 5; then reconsider g1=f1 as Function of I[01],((TOP-REAL 2)|P)|Qa by A96,A109,A112, FUNCT_2:2; A113: f1 is continuous by A107,TOPS_2:def 5; A114: for G being Subset of ((TOP-REAL 2)|P)|Qa st G is open holds g1"G is open proof let G be Subset of ((TOP-REAL 2)|P)|Qa; A115: ((TOP-REAL 2)|P)|Qa=(TOP-REAL 2)|Qa9 by PRE_TOPC:7,XBOOLE_1:36; assume G is open; then consider G4 being Subset of (TOP-REAL 2) such that A116: G4 is open and A117: G=G4 /\ [#]((TOP-REAL 2)|Qa9) by A115,TOPS_2:24; reconsider G5=G4 /\ [#]((TOP-REAL 2)|Segment(P,p1,p2,q,p2)) as Subset of ((TOP-REAL 2)|Segment(P,p1,p2,q,p2)); A118: G5 is open by A116,TOPS_2:24; A119: rng g1=[#]((TOP-REAL 2)|Segment(P,p1,p2,q,p2)) by A107, TOPS_2:def 5 .= Segment(P,p1,p2,q,p2) by PRE_TOPC:def 5; A120: p2 in Segment(P,p1,p2,q,p2) by A106,TOPREAL1:1; A121: f1"G5=g1"(G4 /\ Segment(P,p1,p2,q,p2)) by PRE_TOPC:def 5 .=g1"(G4) /\ g1"(Segment(P,p1,p2,q,p2)) by FUNCT_1:68; g1"G=g1"G4 /\ g1"([#]((TOP-REAL 2)|Qa9)) by A117,FUNCT_1:68 .=g1"G4 /\ g1"Qa9 by PRE_TOPC:def 5 .=g1"G4 /\ g1"((rng g1) /\ Qa9) by RELAT_1:133 .=g1"G4 /\ g1"(Segment(P,p1,p2,q,p2)) by A112,A119,XBOOLE_1:28; hence thesis by A113,A120,A118,A121,TOPS_2:43; end; [#](((TOP-REAL 2)|P)|Qa) <> {}; then A122: g1 is continuous by A114,TOPS_2:43; then q9,p29 are_connected by A108,BORSUK_2:def 1; then g1 is Path of q9,p29 by A108,A122,BORSUK_2:def 2; hence ex G1 being Path of q9,p29 st G1 is continuous & G1.0=q9 & G1 .1=p29 by A108,A122; end; case A123: q=p2; consider g01 being Function of I[01],(((TOP-REAL 2)|P)|Qa) such that A124: g01 is continuous & g01.0=p29 & g01.1=p29 by BORSUK_2:3; p29,p29 are_connected; then g01 is Path of p29,p29 by A124,BORSUK_2:def 2; hence ex G1 being Path of q9,p29 st G1 is continuous & G1.0=q9 & G1 .1=p29 by A123,A124; end; end; then consider G1 being Path of q9,p29 such that A125: G1 is continuous & G1.0=q9 & G1.1=p29; now per cases; case q1<>p1; then A126: Segment(P,p1,p2,p1,q1) is_an_arc_of p1,q1 by A1,A10,JORDAN16:24; then consider f3 being Function of I[01],(TOP-REAL 2)|Segment(P,p1,p2, p1,q1) such that A127: f3 is being_homeomorphism and A128: f3.0=p1 & f3.1=q1 by TOPREAL1:def 1; A129: rng f3=[#]((TOP-REAL 2)|Segment(P,p1,p2,p1,q1)) by A127, TOPS_2:def 5 .=Segment(P,p1,p2,p1,q1) by PRE_TOPC:def 5; {p where p is Point of TOP-REAL 2: LE p1,p,P,p1,p2 & LE p,q1 ,P,p1, p2} c= Qa proof let x be object; assume x in {p where p is Point of TOP-REAL 2: LE p1,p,P,p1, p2 & LE p,q1,P,p1,p2}; then A130: ex p being Point of TOP-REAL 2 st x=p & LE p1,p,P,p1,p2 & LE p,q1,P,p1,p2; then x<>q2 by A1,A2,A3,JORDAN5C:12,JORDAN6:37; then A131: not x in {q2} by TARSKI:def 1; x in P by A130,JORDAN5C:def 3; hence thesis by A131,XBOOLE_0:def 5; end; then A132: Segment(P,p1,p2,p1,q1) c= Qa by JORDAN6:26; A133: the carrier of ((TOP-REAL 2)|P)|Qa=Qa by PRE_TOPC:8; dom f3=the carrier of I[01] by A18,A127,TOPS_2:def 5; then reconsider g3=f3 as Function of I[01],((TOP-REAL 2)|P)|Qa by A129,A133,A132,FUNCT_2:2; A134: f3 is continuous by A127,TOPS_2:def 5; A135: for G being Subset of ((TOP-REAL 2)|P)|Qa st G is open holds g3"G is open proof let G be Subset of ((TOP-REAL 2)|P)|Qa; A136: ((TOP-REAL 2)|P)|Qa=(TOP-REAL 2)|Qa9 by PRE_TOPC:7,XBOOLE_1:36; assume G is open; then consider G4 being Subset of (TOP-REAL 2) such that A137: G4 is open and A138: G=G4 /\ [#]((TOP-REAL 2)|Qa9) by A136,TOPS_2:24; reconsider G5=G4 /\ [#]((TOP-REAL 2)|Segment(P,p1,p2,p1,q1)) as Subset of ((TOP-REAL 2)|Segment(P,p1,p2,p1,q1)); A139: G5 is open by A137,TOPS_2:24; A140: rng g3=[#]((TOP-REAL 2)|Segment(P,p1,p2,p1,q1)) by A127, TOPS_2:def 5 .= Segment(P,p1,p2,p1,q1) by PRE_TOPC:def 5; A141: p1 in Segment(P,p1,p2,p1,q1) by A126,TOPREAL1:1; A142: f3"G5=g3"(G4 /\ Segment(P,p1,p2,p1,q1)) by PRE_TOPC:def 5 .=g3"(G4) /\ g3"(Segment(P,p1,p2,p1,q1)) by FUNCT_1:68; g3"G=g3"G4 /\ g3"([#]((TOP-REAL 2)|Qa9)) by A138,FUNCT_1:68 .=g3"G4 /\ g3"Qa9 by PRE_TOPC:def 5 .=g3"G4 /\ g3"((rng g3) /\ Qa9) by RELAT_1:133 .=g3"G4 /\ g3"(Segment(P,p1,p2,p1,q1)) by A132,A140,XBOOLE_1:28 ; hence thesis by A134,A141,A139,A142,TOPS_2:43; end; [#](((TOP-REAL 2)|P)|Qa) <> {}; then A143: g3 is continuous by A135,TOPS_2:43; then p19,q19 are_connected by A128,BORSUK_2:def 1; then g3 is Path of p19,q19 by A128,A143,BORSUK_2:def 2; hence ex G3 being Path of p19,q19 st G3 is continuous & G3.0=p19 & G3.1=q19 by A128,A143; end; case A144: q1=p1; consider g01 being Function of I[01],(((TOP-REAL 2)|P)|Qa) such that A145: g01 is continuous & g01.0=q19 & g01.1=q19 by BORSUK_2:3; q19,q19 are_connected; then g01 is Path of q19,q19 by A145,BORSUK_2:def 2; hence ex G3 being Path of p19,q19 st G3 is continuous & G3.0=p19 & G3.1=q19 by A144,A145; end; end; then consider G3 being Path of p19,q19 such that A146: G3 is continuous & G3.0=p19 & G3.1=q19; {p where p is Point of TOP-REAL 2: LE q1,p,Q1,q1,q2 & LE p,q,Q1, q1,q2} c= Qa proof let x be object; assume x in {p where p is Point of TOP-REAL 2: LE q1,p,Q1,q1,q2 & LE p,q,Q1,q1,q2}; then A147: ex p being Point of TOP-REAL 2 st x=p & LE q1,p,Q1,q1,q2 & LE p ,q,Q1,q1,q2; now assume A148: x=q2; LE q,q2,Q1,q1,q2 by A2,A20,JORDAN5C:10; hence contradiction by A2,A21,A19,A147,A148,JORDAN5C:12; end; then A149: not x in {q2} by TARSKI:def 1; x in Q1 by A147,JORDAN5C:def 3; hence thesis by A4,A149,XBOOLE_0:def 5; end; then A150: Segment(Q1,q1,q2,q1,q) c= Qa by JORDAN6:26; dom f2=the carrier of I[01] by A18,A99,TOPS_2:def 5; then reconsider g2=f2 as Function of I[01],((TOP-REAL 2)|P)|Qa by A101 ,A97,A150,FUNCT_2:2; A151: f2 is continuous by A99,TOPS_2:def 5; A152: for G being Subset of ((TOP-REAL 2)|P)|Qa st G is open holds g2" G is open proof let G be Subset of ((TOP-REAL 2)|P)|Qa; A153: ((TOP-REAL 2)|P)|Qa=(TOP-REAL 2)|Qa9 by PRE_TOPC:7,XBOOLE_1:36; assume G is open; then consider G4 being Subset of (TOP-REAL 2) such that A154: G4 is open and A155: G=G4 /\ [#]((TOP-REAL 2)|Qa9) by A153,TOPS_2:24; reconsider G5=G4 /\ [#]((TOP-REAL 2)|Segment(Q1,q1,q2,q1,q)) as Subset of ((TOP-REAL 2)|Segment(Q1,q1,q2,q1,q)); A156: G5 is open by A154,TOPS_2:24; A157: rng g2=[#]((TOP-REAL 2)|Segment(Q1,q1,q2,q1,q)) by A99,TOPS_2:def 5 .= Segment(Q1,q1,q2,q1,q) by PRE_TOPC:def 5; A158: q1 in Segment(Q1,q1,q2,q1,q) by A98,TOPREAL1:1; A159: f2"G5=g2"(G4 /\ Segment(Q1,q1,q2,q1,q)) by PRE_TOPC:def 5 .=g2"(G4) /\ g2"(Segment(Q1,q1,q2,q1,q)) by FUNCT_1:68; g2"G=g2"G4 /\ g2"([#]((TOP-REAL 2)|Qa9)) by A155,FUNCT_1:68 .=g2"G4 /\ g2"Qa9 by PRE_TOPC:def 5 .=g2"G4 /\ g2"((rng g2) /\ Qa9) by RELAT_1:133 .=g2"G4 /\ g2"(Segment(Q1,q1,q2,q1,q)) by A150,A157,XBOOLE_1:28; hence thesis by A151,A158,A156,A159,TOPS_2:43; end; [#](((TOP-REAL 2)|P)|Qa) <> {}; then A160: g2 is continuous by A152,TOPS_2:43; then q19,q9 are_connected by A100,BORSUK_2:def 1; then reconsider G2=g2 as Path of q19,q9 by A100,A160,BORSUK_2:def 2; A161: (G2+G1).1=p29 by A125,A100,A160,BORSUK_2:14; A162: (G2+G1) is continuous & (G2+G1).0=q19 by A125,A100,A160,BORSUK_2:14; then A163: (G3+(G2+G1)).1=p29 by A161,A146,BORSUK_2:14; G3+(G2+G1) is continuous & (G3+(G2+G1)).0=p19 by A162,A161,A146, BORSUK_2:14; hence contradiction by A1,A7,A11,A104,A163,Th18; end; end; hence contradiction; end; hence thesis by A2,A6,Th20; end; theorem for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p being Point of TOP-REAL 2,e being Real st q1 is_Lin P,p1,p2,e & q2`1=e & LSeg(q1,q2) c= P & p in LSeg(q1,q2) holds p is_Lin P,p1,p2,e proof let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p be Point of TOP-REAL 2,e be Real; assume that A1: q1 is_Lin P,p1,p2,e and A2: q2`1=e and A3: LSeg(q1,q2) c= P and A4: p in LSeg(q1,q2); A5: q1 in P by A1; A6: q2 in LSeg(q1,q2) by RLTOPSP1:68; A7: q1`1=e by A1; consider p4 being Point of TOP-REAL 2 such that A8: p4`1~~q2; then LSeg(q1,q2) is_an_arc_of q1,q2 by TOPREAL1:9; hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A3,A11,A13,Th25; end; case A15: q1=q2; then LSeg(q1,q2)={q1} by RLTOPSP1:70; hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A11,A5,A15,Th1; end; end; Segment(P,p1,p2,q1,q2) = {p3 where p3 is Point of TOP-REAL 2: LE q1 ,p3,P,p1,p2 & LE p3,q2,P,p1,p2} by JORDAN6:26; then A16: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q1,p3,P,p1, p2 & LE p3, q2,P,p1,p2 by A4,A14; then A17: LE p4,p,P,p1,p2 by A9,JORDAN5C:13; A18: for p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6,p,P,p1 ,p2 holds p6`1<=e proof let p6 be Point of TOP-REAL 2; assume that A19: LE p4,p6,P,p1,p2 and A20: LE p6,p,P,p1,p2; A21: p6 in P by A19,JORDAN5C:def 3; now per cases by A11,A5,A21,Th19; case LE p6,q1,P,p1,p2; hence thesis by A10,A19; end; case A22: LE q1,p6,P,p1,p2; LE p6,q2,P,p1,p2 by A16,A20,JORDAN5C:13; then p6 in {qq where qq is Point of TOP-REAL 2: LE q1,qq,P,p1, p2 & LE qq,q2,P,p1,p2} by A22; then p6 in LSeg(q1,q2) by A14,JORDAN6:26; hence thesis by A2,A7,GOBOARD7:5; end; end; hence thesis; end; p`1=e by A2,A4,A7,GOBOARD7:5; hence thesis by A3,A4,A11,A8,A17,A18; end; case A23: LE q2,q1,P,p1,p2; A24: now per cases; case q1<>q2; then LSeg(q2,q1) is_an_arc_of q2,q1 by TOPREAL1:9; hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A3,A11,A23,Th25; end; case A25: q1=q2; then LSeg(q2,q1)={q1} by RLTOPSP1:70; hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A11,A5,A25,Th1; end; end; A26: now assume LE q2,p4,P,p1,p2; then p4 in {qq where qq is Point of TOP-REAL 2: LE q2,qq,P,p1,p2 & LE qq,q1,P,p1,p2} by A9; then p4 in Segment(P,p1,p2,q2,q1) by JORDAN6:26; hence contradiction by A2,A7,A8,A24,GOBOARD7:5; end; Segment(P,p1,p2,q2,q1) = {p3 where p3 is Point of TOP-REAL 2: LE q2 ,p3,P,p1,p2 & LE p3,q1,P,p1,p2} by JORDAN6:26; then A27: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q2,p3,P,p1, p2 & LE p3, q1,P,p1,p2 by A4,A24; A28: for p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6,p,P,p1 ,p2 holds p6`1<=e proof let p6 be Point of TOP-REAL 2; assume that A29: LE p4,p6,P,p1,p2 and A30: LE p6,p,P,p1,p2; LE p6,q1,P,p1,p2 by A27,A30,JORDAN5C:13; hence thesis by A10,A29; end; LE q2,p4,P,p1,p2 or LE p4,q2,P,p1,p2 by A3,A11,A6,A12,Th19; then A31: LE p4,p,P,p1,p2 by A27,A26,JORDAN5C:13; p`1=e by A2,A4,A7,GOBOARD7:5; hence thesis by A3,A4,A11,A8,A31,A28; end; end; hence thesis; end; theorem for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p being Point of TOP-REAL 2,e being Real st q1 is_Rin P,p1,p2,e & q2`1=e & LSeg(q1,q2) c= P & p in LSeg(q1,q2) holds p is_Rin P,p1,p2,e proof let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p be Point of TOP-REAL 2,e be Real; assume that A1: q1 is_Rin P,p1,p2,e and A2: q2`1=e and A3: LSeg(q1,q2) c= P and A4: p in LSeg(q1,q2); A5: q1 in P by A1; A6: q2 in LSeg(q1,q2) by RLTOPSP1:68; A7: q1`1=e by A1; consider p4 being Point of TOP-REAL 2 such that A8: p4`1>e and A9: LE p4,q1,P,p1,p2 and A10: for p5 being Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5,q1,P, p1,p2 holds p5`1>=e by A1; A11: P is_an_arc_of p1,p2 by A1; A12: p4 in P by A9,JORDAN5C:def 3; now per cases by A3,A11,A5,A6,Th19; case A13: LE q1,q2,P,p1,p2; A14: now per cases; case q1<>q2; then LSeg(q1,q2) is_an_arc_of q1,q2 by TOPREAL1:9; hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A3,A11,A13,Th25; end; case A15: q1=q2; then LSeg(q1,q2)={q1} by RLTOPSP1:70; hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A11,A5,A15,Th1; end; end; Segment(P,p1,p2,q1,q2) = {p3 where p3 is Point of TOP-REAL 2: LE q1 ,p3,P,p1,p2 & LE p3,q2,P,p1,p2} by JORDAN6:26; then A16: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q1,p3,P,p1, p2 & LE p3, q2,P,p1,p2 by A4,A14; then A17: LE p4,p,P,p1,p2 by A9,JORDAN5C:13; A18: for p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6,p,P,p1 ,p2 holds p6`1>=e proof let p6 be Point of TOP-REAL 2; assume that A19: LE p4,p6,P,p1,p2 and A20: LE p6,p,P,p1,p2; A21: p6 in P by A19,JORDAN5C:def 3; now per cases by A11,A5,A21,Th19; case LE p6,q1,P,p1,p2; hence thesis by A10,A19; end; case A22: LE q1,p6,P,p1,p2; LE p6,q2,P,p1,p2 by A16,A20,JORDAN5C:13; then p6 in {qq where qq is Point of TOP-REAL 2: LE q1,qq,P,p1, p2 & LE qq,q2,P,p1,p2} by A22; then p6 in LSeg(q1,q2) by A14,JORDAN6:26; hence thesis by A2,A7,GOBOARD7:5; end; end; hence thesis; end; p`1=e by A2,A4,A7,GOBOARD7:5; hence thesis by A3,A4,A11,A8,A17,A18; end; case A23: LE q2,q1,P,p1,p2; A24: now per cases; case q1<>q2; then LSeg(q2,q1) is_an_arc_of q2,q1 by TOPREAL1:9; hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A3,A11,A23,Th25; end; case A25: q1=q2; then LSeg(q2,q1)={q1} by RLTOPSP1:70; hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A11,A5,A25,Th1; end; end; A26: now assume LE q2,p4,P,p1,p2; then p4 in {qq where qq is Point of TOP-REAL 2: LE q2,qq,P,p1,p2 & LE qq,q1,P,p1,p2} by A9; then p4 in Segment(P,p1,p2,q2,q1) by JORDAN6:26; hence contradiction by A2,A7,A8,A24,GOBOARD7:5; end; Segment(P,p1,p2,q2,q1) = {p3 where p3 is Point of TOP-REAL 2: LE q2 ,p3,P,p1,p2 & LE p3,q1,P,p1,p2} by JORDAN6:26; then A27: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q2,p3,P,p1, p2 & LE p3, q1,P,p1,p2 by A4,A24; A28: for p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6,p,P,p1 ,p2 holds p6`1>=e proof let p6 be Point of TOP-REAL 2; assume that A29: LE p4,p6,P,p1,p2 and A30: LE p6,p,P,p1,p2; LE p6,q1,P,p1,p2 by A27,A30,JORDAN5C:13; hence thesis by A10,A29; end; LE q2,p4,P,p1,p2 or LE p4,q2,P,p1,p2 by A3,A11,A6,A12,Th19; then A31: LE p4,p,P,p1,p2 by A27,A26,JORDAN5C:13; p`1=e by A2,A4,A7,GOBOARD7:5; hence thesis by A3,A4,A11,A8,A31,A28; end; end; hence thesis; end; theorem for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p being Point of TOP-REAL 2,e being Real st q1 is_Lout P,p1,p2,e & q2`1=e & LSeg(q1,q2) c= P & p in LSeg(q1,q2) holds p is_Lout P,p1,p2,e proof let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p be Point of TOP-REAL 2,e be Real; assume that A1: q1 is_Lout P,p1,p2,e and A2: q2`1=e and A3: LSeg(q1,q2) c= P and A4: p in LSeg(q1,q2); A5: q1 in P by A1; A6: q2 in LSeg(q1,q2) by RLTOPSP1:68; A7: q1`1=e by A1; consider p4 being Point of TOP-REAL 2 such that A8: p4`1 q2; then LSeg(q2,q1) is_an_arc_of q2,q1 by TOPREAL1:9; hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A3,A11,A13,Th25; end; case A15: q1=q2; then LSeg(q1,q2)={q1} by RLTOPSP1:70; hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A11,A5,A15,Th1; end; end; Segment(P,p1,p2,q2,q1) = {p3 where p3 is Point of TOP-REAL 2: LE q2 ,p3,P,p1,p2 & LE p3,q1,P,p1,p2} by JORDAN6:26; then A16: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q2,p3,P,p1, p2 & LE p3, q1,P,p1,p2 by A4,A14; then A17: LE p,p4,P,p1,p2 by A9,JORDAN5C:13; A18: for p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p,p6,P,p1 ,p2 holds p6`1<=e proof let p6 be Point of TOP-REAL 2; assume that A19: LE p6,p4,P,p1,p2 and A20: LE p,p6,P,p1,p2; A21: p6 in P by A19,JORDAN5C:def 3; now per cases by A11,A5,A21,Th19; case LE q1,p6,P,p1,p2; hence thesis by A10,A19; end; case A22: LE p6,q1,P,p1,p2; LE q2,p6,P,p1,p2 by A16,A20,JORDAN5C:13; then p6 in {qq where qq is Point of TOP-REAL 2: LE q2,qq,P,p1, p2 & LE qq,q1,P,p1,p2} by A22; then p6 in LSeg(q2,q1) by A14,JORDAN6:26; hence thesis by A2,A7,GOBOARD7:5; end; end; hence thesis; end; p`1=e by A2,A4,A7,GOBOARD7:5; hence thesis by A3,A4,A11,A8,A17,A18; end; case A23: LE q1,q2,P,p1,p2; A24: now per cases; case q1<>q2; then LSeg(q1,q2) is_an_arc_of q1,q2 by TOPREAL1:9; hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A3,A11,A23,Th25; end; case A25: q1=q2; then LSeg(q2,q1)={q1} by RLTOPSP1:70; hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A11,A5,A25,Th1; end; end; A26: now assume LE p4,q2,P,p1,p2; then p4 in {qq where qq is Point of TOP-REAL 2: LE q1,qq,P,p1,p2 & LE qq,q2,P,p1,p2} by A9; then p4 in Segment(P,p1,p2,q1,q2) by JORDAN6:26; hence contradiction by A2,A7,A8,A24,GOBOARD7:5; end; Segment(P,p1,p2,q1,q2) = {p3 where p3 is Point of TOP-REAL 2: LE q1 ,p3,P,p1,p2 & LE p3,q2,P,p1,p2} by JORDAN6:26; then A27: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q1,p3,P,p1, p2 & LE p3, q2,P,p1,p2 by A4,A24; A28: for p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p,p6,P,p1 ,p2 holds p6`1<=e proof let p6 be Point of TOP-REAL 2; assume that A29: LE p6,p4,P,p1,p2 and A30: LE p,p6,P,p1,p2; LE q1,p6,P,p1,p2 by A27,A30,JORDAN5C:13; hence thesis by A10,A29; end; LE q2,p4,P,p1,p2 or LE p4,q2,P,p1,p2 by A3,A11,A6,A12,Th19; then A31: LE p,p4,P,p1,p2 by A27,A26,JORDAN5C:13; p`1=e by A2,A4,A7,GOBOARD7:5; hence thesis by A3,A4,A11,A8,A31,A28; end; end; hence thesis; end; theorem for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p being Point of TOP-REAL 2,e being Real st q1 is_Rout P,p1,p2,e & q2`1=e & LSeg(q1,q2) c= P & p in LSeg(q1,q2) holds p is_Rout P,p1,p2,e proof let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p be Point of TOP-REAL 2,e be Real; assume that A1: q1 is_Rout P,p1,p2,e and A2: q2`1=e and A3: LSeg(q1,q2) c= P and A4: p in LSeg(q1,q2); A5: q1 in P by A1; A6: q2 in LSeg(q1,q2) by RLTOPSP1:68; A7: q1`1=e by A1; consider p4 being Point of TOP-REAL 2 such that A8: p4`1>e and A9: LE q1,p4,P,p1,p2 and A10: for p5 being Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE q1,p5,P, p1,p2 holds p5`1>=e by A1; A11: P is_an_arc_of p1,p2 by A1; A12: p4 in P by A9,JORDAN5C:def 3; now per cases by A3,A11,A5,A6,Th19; case A13: LE q2,q1,P,p1,p2; A14: now per cases; case q1<>q2; then LSeg(q2,q1) is_an_arc_of q2,q1 by TOPREAL1:9; hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A3,A11,A13,Th25; end; case A15: q1=q2; then LSeg(q1,q2)={q1} by RLTOPSP1:70; hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A11,A5,A15,Th1; end; end; Segment(P,p1,p2,q2,q1) = {p3 where p3 is Point of TOP-REAL 2: LE q2 ,p3,P,p1,p2 & LE p3,q1,P,p1,p2} by JORDAN6:26; then A16: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q2,p3,P,p1, p2 & LE p3, q1,P,p1,p2 by A4,A14; then A17: LE p,p4,P,p1,p2 by A9,JORDAN5C:13; A18: for p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p,p6,P,p1 ,p2 holds p6`1>=e proof let p6 be Point of TOP-REAL 2; assume that A19: LE p6,p4,P,p1,p2 and A20: LE p,p6,P,p1,p2; A21: p6 in P by A19,JORDAN5C:def 3; now per cases by A11,A5,A21,Th19; case LE q1,p6,P,p1,p2; hence thesis by A10,A19; end; case A22: LE p6,q1,P,p1,p2; LE q2,p6,P,p1,p2 by A16,A20,JORDAN5C:13; then p6 in {qq where qq is Point of TOP-REAL 2: LE q2,qq,P,p1, p2 & LE qq,q1,P,p1,p2} by A22; then p6 in LSeg(q2,q1) by A14,JORDAN6:26; hence thesis by A2,A7,GOBOARD7:5; end; end; hence thesis; end; p`1=e by A2,A4,A7,GOBOARD7:5; hence thesis by A3,A4,A11,A8,A17,A18; end; case A23: LE q1,q2,P,p1,p2; A24: now per cases; case q1<>q2; then LSeg(q1,q2) is_an_arc_of q1,q2 by TOPREAL1:9; hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A3,A11,A23,Th25; end; case A25: q1=q2; then LSeg(q2,q1)={q1} by RLTOPSP1:70; hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A11,A5,A25,Th1; end; end; A26: now assume LE p4,q2,P,p1,p2; then p4 in {qq where qq is Point of TOP-REAL 2: LE q1,qq,P,p1,p2 & LE qq,q2,P,p1,p2} by A9; then p4 in Segment(P,p1,p2,q1,q2) by JORDAN6:26; hence contradiction by A2,A7,A8,A24,GOBOARD7:5; end; Segment(P,p1,p2,q1,q2) = {p3 where p3 is Point of TOP-REAL 2: LE q1 ,p3,P,p1,p2 & LE p3,q2,P,p1,p2} by JORDAN6:26; then A27: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q1,p3,P,p1, p2 & LE p3, q2,P,p1,p2 by A4,A24; A28: for p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p,p6,P,p1 ,p2 holds p6`1>=e proof let p6 be Point of TOP-REAL 2; assume that A29: LE p6,p4,P,p1,p2 and A30: LE p,p6,P,p1,p2; LE q1,p6,P,p1,p2 by A27,A30,JORDAN5C:13; hence thesis by A10,A29; end; LE q2,p4,P,p1,p2 or LE p4,q2,P,p1,p2 by A3,A11,A6,A12,Th19; then A31: LE p,p4,P,p1,p2 by A27,A26,JORDAN5C:13; p`1=e by A2,A4,A7,GOBOARD7:5; hence thesis by A3,A4,A11,A8,A31,A28; end; end; hence thesis; end; theorem for P being non empty Subset of TOP-REAL 2, p1,p2,p being Point of TOP-REAL 2,e being Real st P is_S-P_arc_joining p1,p2 & p1`1 = 2 by A5,TOPREAL1:def 8; then A10: len f >1 by XXREAL_0:2; A11: L~f = union { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f } by TOPREAL1:def 4; then consider Y being set such that A12: p in Y and A13: Y in { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f } by A3,A6,TARSKI:def 4; consider i being Nat such that A14: Y=LSeg(f,i) and A15: 1 <= i and A16: i+1 <= len f by A13; A17: i-1>=0 by A15,XREAL_1:48; A18: 1 e; A20: i=1 by XREAL_0:def 2; i-'k <=i by NAT_D:35; then A29: i-'k 0 by A20,XREAL_1:50; then len f-'i=len f-i by XREAL_0:def 2; then A41: len f-'i+1>0+1 by A40,XREAL_1:8; A42: len g=len f -'i+1 by A10,A15,A20,FINSEQ_6:118; then A43: 1+1<=len g by A41,NAT_1:13; then 1+1 in Seg len g by FINSEQ_1:1; then 1+1 in dom g by FINSEQ_1:def 3; then A44: g/.(1+1)=g.(1+1) by PARTFUN1:def 6 .=f.(1+1-1+i) by A15,A20,A38,FINSEQ_6:122 .=f/.(i+1) by A37,PARTFUN1:def 6; 1 in dom g by A42,A41,FINSEQ_3:25; then A45: g/.1=g.1 by PARTFUN1:def 6 .=f.(1-1+i) by A15,A36,A39,FINSEQ_6:122 .=f/.i by A21,PARTFUN1:def 6; LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3 .=LSeg(g,1) by A43,A45,A44,TOPREAL1:def 3; then Y in { LSeg(g,i2) where i2 is Nat : 1 <= i2 & i2+1 <= len g } by A14,A43; then p in union{ LSeg(g,i2) where i2 is Nat : 1 <= i2 & i2+1 <= len g } by A12,TARSKI:def 4; then A46: p in L~mid(f,i,len f) by TOPREAL1:def 4; A47: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3; A48: for p5 being Point of TOP-REAL 2 st LE p44,p5,P,p1,p2 & LE p5,p ,P,p1,p2 holds p5`1<=e proof p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68; then LSeg(p44,p) c= LSeg(f,i) by A12,A14,A47,TOPREAL1:6; then A49: LSeg(p44,p) c= P by A6,A19,A14; let p5 be Point of TOP-REAL 2; A50: Segment(P,p1,p2,p44,p)={p8 where p8 is Point of TOP-REAL 2: LE p44,p8,P,p1,p2 & LE p8,p,P,p1,p2} by JORDAN6:26; assume LE p44,p5,P,p1,p2 & LE p5,p,P,p1,p2; then A51: p5 in Segment(P,p1,p2,p44,p) by A50; now per cases; case p44<>p; then LSeg(p44,p) is_an_arc_of p44,p by TOPREAL1:9; then Segment(P,p1,p2,p44,p)=LSeg(p44,p) by A9,A5,A6,A7,A8,A15 ,A20,A46,A49,Th25,SPRECT_4:3; hence thesis by A4,A33,A35,A51,TOPREAL1:3; end; case p44=p; hence thesis by A4,A33,A35; end; end; hence thesis; end; LE p44,p,P,p1,p2 by A5,A6,A7,A8,A15,A20,A46,SPRECT_4:3; hence thesis by A3,A4,A9,A33,A35,A48; end; case A52: k<>0; reconsider ia=i+1 as Nat; reconsider g=mid(f,i,len f) as FinSequence of (TOP-REAL 2); A53: i<=len f by A16,NAT_1:13; ia in Seg len f by A16,A18,FINSEQ_1:1; then A54: i+1 in dom f by FINSEQ_1:def 3; 1+(1+i)<=1+len f by A16,XREAL_1:7; then A55: 1+1+i-i<=len f+1-i by XREAL_1:9; then A56: 1<=len f+1-i by XXREAL_0:2; A57: len f-i>0 by A20,XREAL_1:50; then len f-'i=len f-i by XREAL_0:def 2; then A58: len f-'i+1>0+1 by A57,XREAL_1:8; A59: len g=len f -'i+1 by A10,A15,A20,FINSEQ_6:118; then A60: 1+1<=len g by A58,NAT_1:13; then 1+1 in Seg len g by FINSEQ_1:1; then 1+1 in dom g by FINSEQ_1:def 3; then A61: g/.(1+1)=g.(1+1) by PARTFUN1:def 6 .=f.(1+1-1+i) by A15,A20,A55,FINSEQ_6:122 .=f/.(i+1) by A54,PARTFUN1:def 6; 1 in dom g by A59,A58,FINSEQ_3:25; then A62: g/.1=g.1 by PARTFUN1:def 6 .=f.(1-1+i) by A15,A53,A56,FINSEQ_6:122 .=f/.i by A21,PARTFUN1:def 6; LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3 .=LSeg(g,1) by A60,A62,A61,TOPREAL1:def 3; then Y in { LSeg(g,i2) where i2 is Nat : 1 <= i2 & i2+1 <= len g } by A14,A60; then p in union{ LSeg(g,i2) where i2 is Nat : 1 <= i2 & i2+1 <= len g} by A12,TARSKI:def 4; then A63: p in L~mid(f,i,len f) by TOPREAL1:def 4; reconsider g=mid(f,1,i) as FinSequence of (TOP-REAL 2); set p44=f/.i; A64: i<=len f & 1<=i-'k by A16,A27,NAT_1:13,XREAL_0:def 2; A65: k>=0+1 by A52,NAT_1:13; then A66: i-'k<=i+1-1 by A28,NAT_D:51; A67: i>i-'k by A28,A65,NAT_D:51; then A68: i>1 by A28,XXREAL_0:2; then i-1>0 by XREAL_1:50; then A69: i-'1=i-1 by XREAL_0:def 2; A70: now assume A71: (f/.i)`1<>e; f.i=f/.i by A21,PARTFUN1:def 6; then for p9 being Point of TOP-REAL 2 st p9=f.(i-'0) holds p9`1<>e by A71,NAT_D:40; hence contradiction by A26,A52; end; A72: now assume not for p51 being Point of TOP-REAL 2 st LE pk,p51,P,p1, p2 & LE p51,p44,P,p1,p2 holds p51`1<=e; then consider p51 being Point of TOP-REAL 2 such that A73: LE pk,p51,P,p1,p2 and A74: LE p51,p44,P,p1,p2 and A75: p51`1>e; p51 in P by A73,JORDAN5C:def 3; then consider Y3 being set such that A76: p51 in Y3 and A77: Y3 in { LSeg(f,i5) where i5 is Nat : 1 <= i5 & i5+1 <= len f } by A6,A11,TARSKI:def 4; consider kk being Nat such that A78: Y3=LSeg(f,kk) and A79: 1 <= kk and A80: kk+1 <= len f by A77; A81: LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) by A79,A80,TOPREAL1:def 3; 1 e; A87: LSeg(f/.kk,f/.(kk+1)) c= L~f proof let z be object; assume A88: z in LSeg(f/.kk,f/.(kk+1)); LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is Nat : 1 <= i7 & i7+1 <= len f } by A79,A80,A81; hence thesis by A11,A88,TARSKI:def 4; end; f is special by A5,TOPREAL1:def 8; then A89: (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A79,A80, TOPREAL1:def 5; f is one-to-one & kk f.(kk+1) by A84,A82,FUNCT_1:def 4; A91: LE f/.(i-'k),p51,L~f,f/.1,f/.(len f) by A6,A7,A8,A30,A73, PARTFUN1:def 6; A92: LE f/.(i-'k),f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A31,A73 ,A85,JORDAN5C:13; set k2=i-'kk; LE f/.kk,p51,L~f,f/.1,f/.(len f) by A5,A76,A78,A79,A80, JORDAN5C:25; then A93: LE f/.kk,p44,L~f,f/.1,f/.(len f) by A6,A7,A8,A74,JORDAN5C:13; now assume i-kk<=0; then i-kk+kk<=0+kk by XREAL_1:7; then LE f/.i,f/.kk,L~f,f/.1,f/.(len f) by A5,A68,A83, JORDAN5C:24; hence contradiction by A1,A6,A7,A8,A70,A86,A93,JORDAN5C:12 ,TOPREAL4:2; end; then A94: i-'kk=i-kk by XREAL_0:def 2; then A95: i-k2=i-'k2 by XREAL_0:def 2; i-k2>0 by A79,A94; then i-'k2>0 by XREAL_0:def 2; then i-'k2>=0+1 by NAT_1:13; then P[k2] by A20,A86,A94,A95,FINSEQ_4:15,NAT_D:50; then k2>=k by A26; then i-k2<=i-k by XREAL_1:10; then A96: LE f/.(i-'k2),f/.(i-'k),L~f,f/.1,f/.(len f ) by A5,A29,A32,A79 ,A94,A95,JORDAN5C:24; f/.kk=f.kk & f/.(kk+1)=f.(kk+1) by A84,A82,PARTFUN1:def 6; then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A90, TOPREAL1:9; then A97: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/. kk,f/.(kk+1)) by A9,A6,A7,A8,A94,A95,A96,A92,A87,Th25,JORDAN5C:13; Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~ f,f/.1,f/.(len f)} by JORDAN6:26; then A98: f/.(i-'k) in Segment(L~f,f/.1,f/.(len f),f /.kk,f/.(kk+ 1)) by A94,A95,A96,A92; then (f/.(kk+1))`1 (f/.(kk+1))`1 by A86,XXREAL_0:2; then (f/.(i-'k))`1>=p51`1 by A5,A76,A78,A79,A83,A81,A91,A98,A97 ,A89,Th6; hence contradiction by A31,A33,A75,XXREAL_0:2; end; case A99: (f/.(kk+1))`1 >e & (f/.kk)`1<=e; set k2=i-'kk-'1; A100: LSeg(f/.kk,f/.(kk+1)) c= L~f proof let z be object; assume A101: z in LSeg(f/.kk,f/.(kk+1)); LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is Nat : 1 <= i7 & i7+1 <= len f } by A79,A80,A81; hence thesis by A11,A101,TARSKI:def 4; end; f is one-to-one & kk f.(kk+1) by A84,A82,FUNCT_1:def 4; A103: (f/.kk)`1<(f/.(kk+1))`1 by A99,XXREAL_0:2; LE f/.kk,p51,L~f,f/.1,f/.(len f) by A5,A76,A78,A79,A80, JORDAN5C:25; then A104: LE f/.kk,p44,L~f,f/.1,f/.(len f) by A6,A7,A8,A74,JORDAN5C:13; f/.kk=f.kk & f/.(kk+1)=f.(kk+1) by A84,A82,PARTFUN1:def 6; then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A102 ,TOPREAL1:9; then A105: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~ f,f/.1,f/.(len f)} & Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/.kk, f/.(kk+1)) by A9,A5,A6,A7,A8,A79,A80,A100,Th25,JORDAN5C:23,JORDAN6:26; A106: now assume i-kk-1<=0; then i-(kk+1)+(kk+1)<=0+(kk+1) by XREAL_1:7; then LE f/.i,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A68,A80, JORDAN5C:24; then A107: f/.i in LSeg(f/.kk,f/.(kk+1)) by A105,A104; f is special by A5,TOPREAL1:def 8; then A108: (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A79,A80 ,TOPREAL1:def 5; LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) by A79,A80,TOPREAL1:def 3; hence contradiction by A5,A6,A7,A8,A70,A74,A75,A76,A78,A79 ,A83,A103,A107,A108,Th7; end; then i-kk-1+1>=0+1 by XREAL_1:7; then i-'kk=i-kk by XREAL_0:def 2; then A109: i-k2=i-(i-kk-1) by A106,XREAL_0:def 2 .=kk+1; then i-'k2>0 by XREAL_0:def 2; then A110: i-'k2>=0+1 by NAT_1:13; A111: i-k2=i-'k2 by A109,XREAL_0:def 2; then P[k2] by A20,A99,A109,A110,FINSEQ_4:15,NAT_D:50; then k2>=k by A26; then i-k2<=i-k by XREAL_1:10; then A112: LE f/.(kk+1),f/.(i-'k),L~f,f/.1,f/.(len f) by A5,A29,A32,A109 ,A111,A110,JORDAN5C:24; LE f/.(i-'k),f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A31,A73 ,A85,JORDAN5C:13; hence contradiction by A1,A6,A7,A8,A31,A33,A99,A112,JORDAN5C:12 ,TOPREAL4:2; end; end; hence contradiction; end; A113: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3; A114: for p5 being Point of TOP-REAL 2 st LE p44,p5,P,p1,p2 & LE p5, p,P,p1,p2 holds p5`1<=e proof let p5 be Point of TOP-REAL 2; A115: Segment(P,p1,p2,p44,p)={p8 where p8 is Point of TOP-REAL 2: LE p44,p8,P,p1,p2 & LE p8,p,P,p1,p2} by JORDAN6:26; assume LE p44,p5,P,p1,p2 & LE p5,p,P,p1,p2; then A116: p5 in Segment(P,p1,p2,p44,p) by A115; p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68; then LSeg(p44,p) c= LSeg(f,i) by A12,A14,A113,TOPREAL1:6; then A117: LSeg(p44,p) c= P by A6,A19,A14; now per cases; case p44<>p; then LSeg(p44,p) is_an_arc_of p44,p by TOPREAL1:9; then Segment(P,p1,p2,p44,p)=LSeg(p44,p) by A9,A5,A6,A7,A8,A15 ,A20,A63,A117,Th25,SPRECT_4:3; hence thesis by A4,A70,A116,TOPREAL1:3; end; case p44=p; then Segment(P,p1,p2,p44,p)={p44} by A1,A3,Th1,TOPREAL4:2; hence thesis by A70,A116,TARSKI:def 1; end; end; hence thesis; end; A118: len g=i -'1+1 by A15,A20,A22,FINSEQ_6:118; then i-'k+1<=len g by A67,A69,NAT_1:13; then A119: LSeg(g,i-'k)=LSeg(g/.(i-'k),g/.(i-'k+1)) by A28,TOPREAL1:def 3; i-'k e; now per cases; case A129: k=0; set p44=f/.i; A130: pk=f.i by A129,NAT_D:40 .=p44 by A21,PARTFUN1:def 6; reconsider ia=i+1 as Nat; reconsider g=mid(f,i,len f) as FinSequence of (TOP-REAL 2); A131: i<=len f by A16,NAT_1:13; ia in Seg len f by A16,A18,FINSEQ_1:1; then A132: i+1 in dom f by FINSEQ_1:def 3; 1+(1+i)<=1+len f by A16,XREAL_1:7; then A133: 1+1+i-i<=len f+1-i by XREAL_1:9; then A134: 1<=len f+1-i by XXREAL_0:2; A135: len f-i>0 by A20,XREAL_1:50; then len f-'i=len f-i by XREAL_0:def 2; then A136: len f-'i+1>0+1 by A135,XREAL_1:8; A137: len g=len f -'i+1 by A10,A15,A20,FINSEQ_6:118; then A138: 1+1<=len g by A136,NAT_1:13; then 1+1 in Seg len g by FINSEQ_1:1; then 1+1 in dom g by FINSEQ_1:def 3; then A139: g/.(1+1)=g.(1+1) by PARTFUN1:def 6 .=f.(1+1-1+i) by A15,A20,A133,FINSEQ_6:122 .=f/.(i+1) by A132,PARTFUN1:def 6; 1 in Seg len g by A137,A136,FINSEQ_1:1; then 1 in dom g by FINSEQ_1:def 3; then A140: g/.1=g.1 by PARTFUN1:def 6 .=f.(1-1+i) by A15,A131,A134,FINSEQ_6:122 .=f/.i by A21,PARTFUN1:def 6; LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3 .=LSeg(g,1) by A138,A140,A139,TOPREAL1:def 3; then Y in { LSeg(g,i2) where i2 is Nat : 1 <= i2 & i2+1 <= len g } by A14,A138; then p in union{ LSeg(g,i2) where i2 is Nat : 1 <= i2 & i2+1 <= len g } by A12,TARSKI:def 4; then A141: p in L~mid(f,i,len f) by TOPREAL1:def 4; A142: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3; A143: for p5 being Point of TOP-REAL 2 st LE p44,p5,P,p1,p2 & LE p5, p,P,p1,p2 holds p5`1>=e proof p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68; then LSeg(p44,p) c= LSeg(f,i) by A12,A14,A142,TOPREAL1:6; then A144: LSeg(p44,p) c= P by A6,A19,A14; let p5 be Point of TOP-REAL 2; A145: Segment(P,p1,p2,p44,p)={p8 where p8 is Point of TOP-REAL 2: LE p44,p8,P,p1,p2 & LE p8,p,P,p1,p2} by JORDAN6:26; assume LE p44,p5,P,p1,p2 & LE p5,p,P,p1,p2; then A146: p5 in Segment(P,p1,p2,p44,p) by A145; now per cases; case p44<>p; then LSeg(p44,p) is_an_arc_of p44,p by TOPREAL1:9; then Segment(P,p1,p2,p44,p)=LSeg(p44,p) by A9,A5,A6,A7,A8,A15 ,A20,A141,A144,Th25,SPRECT_4:3; hence thesis by A4,A128,A130,A146,TOPREAL1:3; end; case p44=p; hence thesis by A4,A128,A130; end; end; hence thesis; end; LE p44,p,P,p1,p2 by A5,A6,A7,A8,A15,A20,A141,SPRECT_4:3; hence thesis by A3,A4,A9,A128,A130,A143; end; case A147: k<>0; reconsider ia=i+1 as Nat; reconsider g=mid(f,i,len f) as FinSequence of (TOP-REAL 2); A148: i<=len f by A16,NAT_1:13; ia in Seg len f by A16,A18,FINSEQ_1:1; then A149: i+1 in dom f by FINSEQ_1:def 3; 1+(1+i)<=1+len f by A16,XREAL_1:7; then A150: 1+1+i-i<=len f+1-i by XREAL_1:9; then A151: 1<=len f+1-i by XXREAL_0:2; A152: len f-i>0 by A20,XREAL_1:50; then len f-'i=len f-i by XREAL_0:def 2; then A153: len f-'i+1>0+1 by A152,XREAL_1:8; A154: len g=len f -'i+1 by A10,A15,A20,FINSEQ_6:118; then A155: 1+1<=len g by A153,NAT_1:13; then 1+1 in Seg len g by FINSEQ_1:1; then 1+1 in dom g by FINSEQ_1:def 3; then A156: g/.(1+1)=g.(1+1) by PARTFUN1:def 6 .=f.(1+1-1+i) by A15,A20,A150,FINSEQ_6:122 .=f/.(i+1) by A149,PARTFUN1:def 6; 1 in Seg len g by A154,A153,FINSEQ_1:1; then 1 in dom g by FINSEQ_1:def 3; then A157: g/.1=g.1 by PARTFUN1:def 6 .=f.(1-1+i) by A15,A148,A151,FINSEQ_6:122 .=f/.i by A21,PARTFUN1:def 6; LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3 .=LSeg(g,1) by A155,A157,A156,TOPREAL1:def 3; then Y in { LSeg(g,i2) where i2 is Nat : 1 <= i2 & i2+1 <= len g } by A14,A155; then p in union{ LSeg(g,i2) where i2 is Nat : 1 <= i2 & i2+1 <= len g } by A12,TARSKI:def 4; then A158: p in L~mid(f,i,len f) by TOPREAL1:def 4; reconsider g=mid(f,1,i) as FinSequence of (TOP-REAL 2); set p44=f/.i; A159: i<=len f & 1<=i-'k by A16,A27,NAT_1:13,XREAL_0:def 2; A160: k>=0+1 by A147,NAT_1:13; then A161: i-'k<=i+1-1 by A28,NAT_D:51; A162: i>i-'k by A28,A160,NAT_D:51; then A163: i>1 by A28,XXREAL_0:2; then i-1>0 by XREAL_1:50; then A164: i-'1=i-1 by XREAL_0:def 2; A165: now assume A166: (f/.i)`1<>e; f.i=f/.i by A21,PARTFUN1:def 6; then for p9 being Point of TOP-REAL 2 st p9=f.(i-'0) holds p9`1<> e by A166,NAT_D:40; hence contradiction by A26,A147; end; A167: now assume not for p51 being Point of TOP-REAL 2 st LE pk,p51,P,p1, p2 & LE p51,p44,P,p1,p2 holds p51`1>=e; then consider p51 being Point of TOP-REAL 2 such that A168: LE pk,p51,P,p1,p2 and A169: LE p51,p44,P,p1,p2 and A170: p51`1=k by A26; then i-k2<=i-k by XREAL_1:10; then A185: LE f/.(i-'k2),f/.(i-'k),L~f,f/.1,f/.(len f ) by A5,A29,A32,A174 ,A183,A184,JORDAN5C:24; A186: LSeg(f/.kk,f/.(kk+1)) c= L~f proof let z be object; assume A187: z in LSeg(f/.kk,f/.(kk+1)); LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is Nat : 1 <= i7 & i7+1 <= len f } by A174,A175,A176; hence thesis by A11,A187,TARSKI:def 4; end; f is special by A5,TOPREAL1:def 8; then A188: (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A174,A175 ,TOPREAL1:def 5; f is one-to-one & kk f.(kk+1) by A179,A177,FUNCT_1:def 4; A190: LE f/.(i-'k),p51,L~f,f/.1,f/.(len f) by A6,A7,A8,A30,A168, PARTFUN1:def 6; A191: LE f/.(i-'k),f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A31,A168 ,A180,JORDAN5C:13; f/.kk=f.kk & f/.(kk+1)=f.(kk+1) by A179,A177,PARTFUN1:def 6; then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A189 ,TOPREAL1:9; then A192: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/. kk,f/.(kk+1)) by A9,A6,A7,A8,A183,A184,A185,A191,A186,Th25,JORDAN5C:13; Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~ f,f/.1,f/.(len f)} by JORDAN6:26; then A193: f/.(i-'k) in Segment(L~f,f/.1,f/.(len f),f /.kk,f/.(kk+ 1)) by A183,A184,A185,A191; then (f/.(kk+1))`1>e by A31,A128,A181,A192,Th2; then (f/.kk)`1< (f/.(kk+1))`1 by A181,XXREAL_0:2; then (f/.(i-'k))`1<=p51`1 by A5,A171,A173,A174,A178,A176,A190 ,A193,A192,A188,Th7; hence contradiction by A31,A128,A170,XXREAL_0:2; end; case A194: (f/.(kk+1))`1 =e; set k2=i-'kk-'1; A195: LSeg(f/.kk,f/.(kk+1)) c= L~f proof let z be object; assume A196: z in LSeg(f/.kk,f/.(kk+1)); LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is Nat : 1 <= i7 & i7+1 <= len f } by A174,A175,A176; hence thesis by A11,A196,TARSKI:def 4; end; f is one-to-one & kk f.(kk+1) by A179,A177,FUNCT_1:def 4; A198: (f/.kk)`1>(f/.(kk+1))`1 by A194,XXREAL_0:2; LE f/.kk,p51,L~f,f/.1,f/.(len f) by A5,A171,A173,A174,A175, JORDAN5C:25; then A199: LE f/.kk,p44,L~f,f/.1,f/.(len f) by A6,A7,A8,A169,JORDAN5C:13; f/.kk=f.kk & f/.(kk+1)=f.(kk+1) by A179,A177,PARTFUN1:def 6; then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A197 ,TOPREAL1:9; then A200: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~ f,f/.1,f/.(len f)} & Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/.kk, f/.(kk+1)) by A9,A5,A6,A7,A8,A174,A175,A195,Th25,JORDAN5C:23,JORDAN6:26; A201: now assume i-kk-1<=0; then i-(kk+1)+(kk+1)<=0+(kk+1) by XREAL_1:7; then LE f/.i,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A163,A175, JORDAN5C:24; then A202: f/.i in LSeg(f/.kk,f/.(kk+1)) by A200,A199; f is special by A5,TOPREAL1:def 8; then A203: (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A174 ,A175,TOPREAL1:def 5; LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) by A174,A175,TOPREAL1:def 3; hence contradiction by A5,A6,A7,A8,A165,A169,A170,A171,A173 ,A174,A178,A198,A202,A203,Th6; end; then i-kk-1+1>=0+1 by XREAL_1:7; then i-'kk=i-kk by XREAL_0:def 2; then A204: i-k2=i-(i-kk-1) by A201,XREAL_0:def 2 .=kk+1; then i-'k2>0 by XREAL_0:def 2; then A205: i-'k2>=0+1 by NAT_1:13; A206: i-k2=i-'k2 by A204,XREAL_0:def 2; then P[k2] by A20,A194,A204,A205,FINSEQ_4:15,NAT_D:50; then k2>=k by A26; then i-k2<=i-k by XREAL_1:10; then A207: LE f/.(kk+1),f/.(i-'k),L~f,f/.1,f/.(len f) by A5,A29,A32,A204 ,A206,A205,JORDAN5C:24; LE f/.(i-'k),f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A31,A168 ,A180,JORDAN5C:13; hence contradiction by A1,A6,A7,A8,A31,A128,A194,A207, JORDAN5C:12,TOPREAL4:2; end; end; hence contradiction; end; A208: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3; A209: for p5 being Point of TOP-REAL 2 st LE p44,p5,P,p1,p2 & LE p5, p,P,p1,p2 holds p5`1>=e proof let p5 be Point of TOP-REAL 2; A210: Segment(P,p1,p2,p44,p)={p8 where p8 is Point of TOP-REAL 2: LE p44,p8,P,p1,p2 & LE p8,p,P,p1,p2} by JORDAN6:26; assume LE p44,p5,P,p1,p2 & LE p5,p,P,p1,p2; then A211: p5 in Segment(P,p1,p2,p44,p) by A210; p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68; then LSeg(p44,p) c= LSeg(f,i) by A12,A14,A208,TOPREAL1:6; then A212: LSeg(p44,p) c= P by A6,A19,A14; now per cases; case p44<>p; then LSeg(p44,p) is_an_arc_of p44,p by TOPREAL1:9; then Segment(P,p1,p2,p44,p)=LSeg(p44,p) by A9,A5,A6,A7,A8,A15 ,A20,A158,A212,Th25,SPRECT_4:3; hence thesis by A4,A165,A211,TOPREAL1:3; end; case p44=p; then Segment(P,p1,p2,p44,p)={p44} by A1,A3,Th1,TOPREAL4:2; hence thesis by A165,A211,TARSKI:def 1; end; end; hence thesis; end; A213: len g=i -'1+1 by A15,A20,A22,FINSEQ_6:118; then i-'k+1<=len g by A162,A164,NAT_1:13; then A214: LSeg(g,i-'k)=LSeg(g/.(i-'k),g/.(i-'k+1)) by A28,TOPREAL1:def 3; i-'k =e proof let p5 be Point of TOP-REAL 2; assume that A220: LE pk,p5,P,p1,p2 and A221: LE p5,p,P,p1,p2; A222: p5 in P by A220,JORDAN5C:def 3; now per cases by A1,A218,A222,Th19,TOPREAL4:2; case LE p5,p44,P,p1,p2; hence thesis by A167,A220; end; case LE p44,p5,P,p1,p2; hence thesis by A209,A221; end; end; hence thesis; end; LE p44,p,P,p1,p2 by A5,A6,A7,A8,A15,A20,A158,SPRECT_4:3; then LE pk,p,P,p1,p2 by A217,JORDAN5C:13; hence thesis by A3,A4,A9,A128,A219; end; end; hence thesis; end; end; hence thesis; end; theorem for P being non empty Subset of TOP-REAL 2, p1,p2,p being Point of TOP-REAL 2,e being Real st P is_S-P_arc_joining p1,p2 & p2`1>e & p in P & p`1=e holds p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e proof let P be non empty Subset of TOP-REAL 2, p1,p2,p be Point of TOP-REAL 2,e be Real; assume that A1: P is_S-P_arc_joining p1,p2 and A2: p2`1>e and A3: p in P and A4: p`1=e; consider f being FinSequence of (TOP-REAL 2) such that A5: f is being_S-Seq and A6: P = L~f and A7: p1=f/.1 and A8: p2=f/.len f by A1,TOPREAL4:def 1; A9: P is_an_arc_of p1,p2 by A1,TOPREAL4:2; A10: L~f = union { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f } by TOPREAL1:def 4; then consider Y being set such that A11: p in Y and A12: Y in { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f } by A3,A6,TARSKI:def 4; consider i being Nat such that A13: Y=LSeg(f,i) and A14: 1 <= i and A15: i+1 <= len f by A12; A16: 1e; A20: len f - (i+1)>=0 by A15,XREAL_1:48; then A21: i+1+((len f)-'(i+1))=i+1+(len f -(i+1)) by XREAL_0:def 2 .=len f; A22: len f -'(i+1)=len f -(i+1) by A20,XREAL_0:def 2; A23: i=i by NAT_1:11; then A29: i+k+1 >=i+1 by XREAL_1:7; then A30: i+1+k >1 by A16,XXREAL_0:2; 1<=i+1+k by A17,NAT_1:12; then i+1+k in Seg len f by A28,FINSEQ_1:1; then A31: i+1+k in dom f by FINSEQ_1:def 3; then A32: f/.(i+1+k)=f.(i+1+k) by PARTFUN1:def 6; then reconsider pk=f.(i+1+k) as Point of TOP-REAL 2; A33: k+i+1>1 by A16,A29,XXREAL_0:2; now per cases by A26,XXREAL_0:1; case A34: pk`1 p; then LSeg(p,p44) is_an_arc_of p,p44 by TOPREAL1:9; then Segment(P,p1,p2,p,p44)=LSeg(p,p44) by A9,A5,A6,A7,A8,A11,A13 ,A14,A23,A37,A40,Th25,SPRECT_4:4; hence thesis by A4,A34,A36,A42,TOPREAL1:3; end; case p44=p; hence thesis by A4,A18,A34,A35,PARTFUN1:def 6; end; end; hence thesis; end; LE p,p44,P,p1,p2 by A5,A6,A7,A8,A11,A13,A14,A23,A37,SPRECT_4:4; hence thesis by A3,A4,A9,A34,A36,A39; end; case A43: k<>0; set p44=f/.(i+1); A44: now assume (f/.(i+1))`1<>e; then for p9 being Point of TOP-REAL 2 st p9=f.(i+1+0) holds p9`1<> e by A18,PARTFUN1:def 6; hence contradiction by A27,A43; end; A45: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A14,A15,TOPREAL1:def 3; A46: now assume not for p51 being Point of TOP-REAL 2 st LE p44,p51,P,p1, p2 & LE p51,pk,P,p1,p2 holds p51`1<=e; then consider p51 being Point of TOP-REAL 2 such that A47: LE p44,p51,P,p1,p2 and A48: LE p51,pk,P,p1,p2 and A49: p51`1>e; p51 in P by A47,JORDAN5C:def 3; then consider Y3 being set such that A50: p51 in Y3 and A51: Y3 in { LSeg(f,i5) where i5 is Nat : 1 <= i5 & i5+1 <= len f } by A6,A10,TARSKI:def 4; consider kk being Nat such that A52: Y3=LSeg(f,kk) and A53: 1 <= kk and A54: kk+1 <= len f by A51; A55: LE p51,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A50,A52,A53,A54, JORDAN5C:26; A56: LE f/.kk,p51,L~f,f/.1,f/.(len f) by A5,A50,A52,A53,A54,JORDAN5C:25; A57: kk-1>=0 by A53,XREAL_1:48; A58: LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) by A53,A54,TOPREAL1:def 3; A59: kk f.(kk+1) by A60,A63,FUNCT_1:def 4; now per cases by A49,A50,A52,A58,Th2; case A65: (f/.(kk+1))`1>e; set k2=kk-'i; A66: LE p44,f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A47,A55, JORDAN5C:13; now assume kk-i<0; then kk-i+i<0+i by XREAL_1:6; then LE f/.(kk+1),f/.(i+1),L~f,f/.1,f/.(len f) by A5,A15,A62, JORDAN5C:24,XREAL_1:7; hence contradiction by A1,A6,A7,A8,A44,A65,A66,JORDAN5C:12 ,TOPREAL4:2; end; then A67: i+1+k2=1+i+(kk-i) by XREAL_0:def 2 .=kk+1; A68: LSeg(f/.kk,f/.(kk+1)) c= L~f proof let z be object; assume A69: z in LSeg(f/.kk,f/.(kk+1)); LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is Nat : 1 <= i7 & i7+1 <= len f } by A53,A54,A58; hence thesis by A10,A69,TARSKI:def 4; end; f is special by A5,TOPREAL1:def 8; then A70: (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A53,A54, TOPREAL1:def 5; f is one-to-one & kk f.(kk+1) by A60,A63,FUNCT_1:def 4; A72: LE p51,f/.(i+1+k),L~f,f/.1,f/.(len f) by A6,A7,A8,A31,A48, PARTFUN1:def 6; A73: LE f/.(kk),f/.(i+1+k),L~f,f/.1,f/.(len f) by A6,A7,A8,A32,A48 ,A56,JORDAN5C:13; 1 =k by A27; then A74: LE f/.(i+1+k),f/.(i+1+k2),L~f,f/.1,f/.(len f) by A5,A33,A54,A67 ,JORDAN5C:24,XREAL_1:7; f/.kk=f.kk & f/.(kk+1)=f.(kk+1) by A60,A63,PARTFUN1:def 6; then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A71, TOPREAL1:9; then A75: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/. kk,f/.(kk+1)) by A9,A6,A7,A8,A67,A74,A73,A68,Th25,JORDAN5C:13; Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~ f,f/.1,f/.(len f)} by JORDAN6:26; then A76: f/.(i+1+k) in Segment(L~f,f/.1,f/.(len f), f/.kk,f/.(kk + 1)) by A67,A74,A73; then (f/.(kk))`1 =p51`1 by A5,A50,A52,A53,A59,A58,A72,A76 ,A75,A70,Th7; hence contradiction by A32,A34,A49,XXREAL_0:2; end; case A77: (f/.(kk))`1 >e & (f/.(kk+1))`1<=e; set k2=kk-'(i+1); A78: LSeg(f/.kk,f/.(kk+1)) c= L~f proof let z be object; assume A79: z in LSeg(f/.kk,f/.(kk+1)); LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is Nat : 1 <= i7 & i7+1 <= len f } by A53,A54,A58; hence thesis by A10,A79,TARSKI:def 4; end; LE p51,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A50,A52,A53,A54, JORDAN5C:26; then A80: LE p44,f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A47, JORDAN5C:13; f/.(kk+1)=f.(kk+1) by A63,PARTFUN1:def 6; then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A64 ,A61,TOPREAL1:9; then A81: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~ f,f/.1,f/.(len f)} & Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/.kk, f/.(kk+1)) by A9,A5,A6,A7,A8,A53,A54,A78,Th25,JORDAN5C:23,JORDAN6:26; A82: now assume kk-(i+1)<0; then kk-(i+1)+(i+1)<0+(i+1) by XREAL_1:6; then kk<=i by NAT_1:13; then A83: LE f/.kk,f/.i,L~f,f/.1,f/.(len f) by A5,A23,A53,JORDAN5C:24; A84: f/.i in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68; LE f/.i,p44,L~f,f/.1,f/.(len f) by A5,A14,A15,JORDAN5C:23; then LE f/.i,f/.(kk+1),L~f,f/.1,f/.(len f) by A80,JORDAN5C:13 ; then f/.i in LSeg(f/.kk,f/.(kk+1)) by A81,A83; then LSeg(f/.kk,f/.(kk+1)) /\ LSeg(f/.i,f/.(i+1))<>{} by A84, XBOOLE_0:def 4; then A85: not LSeg(f/.kk,f/.(kk+1)) misses LSeg (f/.i,f/.(i+1) ) by XBOOLE_0:def 7; A86: kk-1=kk-'1 by A57,XREAL_0:def 2; A87: now assume A88: i=kk-'1+2; then kk+1 =kk by A85,A90,TOPREAL1:def 7; then A92: i+1-1>=kk-1 by XREAL_1:9; kk+1>=i by A85,A91,A90,TOPREAL1:def 7; then A93: i=kk-'1+0 or ... or i=kk-'1+2 by A86,A92,NAT_1:62; A94: now per cases by A86,A93,A87; case i=kk; hence p44 in LSeg(f,kk) by A45,RLTOPSP1:68; end; case i=kk-1; hence p44 in LSeg(f,kk) by A58,RLTOPSP1:68; end; end; f is special by A5,TOPREAL1:def 8; then (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A53,A54,TOPREAL1:def 5; hence contradiction by A5,A6,A7,A8,A44,A47,A49,A50,A52,A53 ,A59,A77,A94,Th6; end; then i+1+k2=i+1+(kk-(i+1)) by XREAL_0:def 2 .=kk; then P[k2] by A53,A59,A77,FINSEQ_4:15; then A95: k2>=k by A27; kk-'(i+1)=kk-(i+1) by A82,XREAL_0:def 2; then kk-(i+1)+(i+1)>=k+(i+1) by A95,XREAL_1:7; then A96: LE f/.(i+1+k),f/.(kk),L~f,f/.1,f/.(len f) by A5,A30,A59, JORDAN5C:24; LE f/.(kk),f/.(i+1+k),L~f,f/.1,f/.(len f) by A6,A7,A8,A32,A48 ,A56,JORDAN5C:13; hence contradiction by A1,A6,A7,A8,A32,A34,A77,A96,JORDAN5C:12 ,TOPREAL4:2; end; end; hence contradiction; end; A97: p44 in LSeg(p,f/.(i+1)) by RLTOPSP1:68; A98: for p5 being Point of TOP-REAL 2 st LE p,p5,P,p1,p2 & LE p5,p44 ,P,p1,p2 holds p5`1<=e proof let p5 be Point of TOP-REAL 2; A99: Segment(P,p1,p2,p,p44)={p8 where p8 is Point of TOP-REAL 2: LE p,p8,P,p1,p2 & LE p8,p44,P,p1,p2} by JORDAN6:26; assume LE p,p5,P,p1,p2 & LE p5,p44,P,p1,p2; then A100: p5 in Segment(P,p1,p2,p,p44) by A99; p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68; then LSeg(p,p44) c= LSeg(f,i) by A11,A13,A45,TOPREAL1:6; then A101: LSeg(p,p44) c= P by A6,A19,A13; now per cases; case p44<>p; then LSeg(p,p44) is_an_arc_of p,p44 by TOPREAL1:9; then Segment(P,p1,p2,p,p44)=LSeg(p,p44) by A9,A5,A6,A7,A8,A11,A13 ,A14,A23,A97,A101,Th25,SPRECT_4:4; hence thesis by A4,A44,A100,TOPREAL1:3; end; case p44=p; then Segment(P,p1,p2,p,p44)={p44} by A1,A3,Th1,TOPREAL4:2; hence thesis by A44,A100,TARSKI:def 1; end; end; hence thesis; end; i+1<=i+1+k by NAT_1:11; then A102: LE p44,pk,P,p1,p2 by A5,A6,A7,A8,A17,A28,A32,JORDAN5C:24; then A103: p44 in P by JORDAN5C:def 3; A104: for p5 being Point of TOP-REAL 2 st LE p5,pk,P,p1,p2 & LE p,p5 ,P,p1,p2 holds p5`1<=e proof let p5 be Point of TOP-REAL 2; assume that A105: LE p5,pk,P,p1,p2 and A106: LE p,p5,P,p1,p2; A107: p5 in P by A105,JORDAN5C:def 3; now per cases by A1,A103,A107,Th19,TOPREAL4:2; case LE p44,p5,P,p1,p2; hence thesis by A46,A105; end; case LE p5,p44,P,p1,p2; hence thesis by A98,A106; end; end; hence thesis; end; LE p,p44,P,p1,p2 by A5,A6,A7,A8,A11,A13,A14,A23,A97,SPRECT_4:4; then LE p,pk,P,p1,p2 by A102,JORDAN5C:13; hence thesis by A3,A4,A9,A34,A104; end; end; hence thesis; end; case A108: pk`1>e; now per cases; case A109: k=0; set p44=f/.(i+1); A110: pk=p44 by A18,A109,PARTFUN1:def 6; A111: p44 in LSeg(p,f/.(i+1)) by RLTOPSP1:68; A112: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A14,A15,TOPREAL1:def 3; A113: for p5 being Point of TOP-REAL 2 st LE p5,p44,P,p1,p2 & LE p, p5,P,p1,p2 holds p5`1>=e proof p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68; then LSeg(p,p44) c= LSeg(f,i) by A11,A13,A112,TOPREAL1:6; then A114: LSeg(p,p44) c= P by A6,A19,A13; let p5 be Point of TOP-REAL 2; A115: Segment(P,p1,p2,p,p44)={p8 where p8 is Point of TOP-REAL 2: LE p,p8,P,p1,p2 & LE p8,p44,P,p1,p2} by JORDAN6:26; assume LE p5,p44,P,p1,p2 & LE p,p5,P,p1,p2; then A116: p5 in Segment(P,p1,p2,p,p44) by A115; now per cases; case p44<>p; then LSeg(p,p44) is_an_arc_of p,p44 by TOPREAL1:9; then Segment(P,p1,p2,p,p44)=LSeg(p,p44) by A9,A5,A6,A7,A8,A11 ,A13,A14,A23,A111,A114,Th25,SPRECT_4:4; hence thesis by A4,A108,A110,A116,TOPREAL1:3; end; case p44=p; hence thesis by A4,A18,A108,A109,PARTFUN1:def 6; end; end; hence thesis; end; LE p,p44,P,p1,p2 by A5,A6,A7,A8,A11,A13,A14,A23,A111,SPRECT_4:4; hence thesis by A3,A4,A9,A108,A110,A113; end; case A117: k<>0; set p44=f/.(i+1); A118: now assume (f/.(i+1))`1<>e; then for p9 being Point of TOP-REAL 2 st p9=f.(i+1+0) holds p9`1 <>e by A18,PARTFUN1:def 6; hence contradiction by A27,A117; end; A119: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A14,A15,TOPREAL1:def 3; A120: now assume not for p51 being Point of TOP-REAL 2 st LE p44,p51,P,p1 ,p2 & LE p51,pk,P,p1,p2 holds p51`1>=e; then consider p51 being Point of TOP-REAL 2 such that A121: LE p44,p51,P,p1,p2 and A122: LE p51,pk,P,p1,p2 and A123: p51`1=0 by A127,XREAL_1:48; A132: LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) by A127,A128,TOPREAL1:def 3; A133: kk f.(kk+1) by A134,A137,FUNCT_1:def 4; now per cases by A123,A124,A126,A132,Th3; case A139: (f/.(kk+1))`1 f.(kk+1) by A134,A137,FUNCT_1:def 4; A146: LE p51,f/.(i+1+k),L~f,f/.1,f/.(len f) by A6,A7,A8,A31,A122, PARTFUN1:def 6; A147: LE f/.(kk),f/.(i+1+k),L~f,f/.1,f/.(len f) by A6,A7,A8,A32,A122 ,A130,JORDAN5C:13; 1 =k by A27; then A148: LE f/.(i+1+k),f/.(i+1+k2),L~f,f/.1,f/.(len f) by A5,A33,A128 ,A141,JORDAN5C:24,XREAL_1:7; f/.kk=f.kk & f/.(kk+1)=f.(kk+1) by A134,A137,PARTFUN1:def 6; then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A145 ,TOPREAL1:9; then A149: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/. kk,f/.(kk+1)) by A9,A6,A7,A8,A141,A148,A147,A142,Th25,JORDAN5C:13; Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~ f,f/.1,f/.(len f)} by JORDAN6:26; then A150: f/.(i+1+k) in Segment(L~f,f/.1,f/.(len f), f/.kk,f/.(kk +1)) by A141,A148,A147; then (f/.(kk))`1>e by A32,A108,A139,A149,Th2; then (f/.kk)`1> (f/.(kk+1))`1 by A139,XXREAL_0:2; then (f/.(i+1+k))`1<=p51`1 by A5,A124,A126,A127,A133,A132,A146 ,A150,A149,A144,Th6; hence contradiction by A32,A108,A123,XXREAL_0:2; end; case A151: (f/.(kk))`1 =e; set k2=kk-'(i+1); A152: LSeg(f/.kk,f/.(kk+1)) c= L~f proof let z be object; assume A153: z in LSeg(f/.kk,f/.(kk+1)); LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is Nat : 1 <= i7 & i7+1 <= len f } by A127,A128,A132; hence thesis by A10,A153,TARSKI:def 4; end; LE p51,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A124,A126,A127,A128, JORDAN5C:26; then A154: LE p44,f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A121, JORDAN5C:13; f/.(kk+1)=f.(kk+1) by A137,PARTFUN1:def 6; then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A138 ,A135,TOPREAL1:9; then A155: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~ f,f/.1,f/.(len f)} & Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/.kk, f/.(kk+1)) by A9,A5,A6,A7,A8,A127,A128,A152,Th25,JORDAN5C:23,JORDAN6:26; A156: now assume kk-(i+1)<0; then kk-(i+1)+(i+1)<0+(i+1) by XREAL_1:6; then kk<=i by NAT_1:13; then A157: LE f/.kk,f/.i,L~f,f/.1,f/.(len f) by A5,A23,A127,JORDAN5C:24; A158: f/.i in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68; LE f/.i,p44,L~f,f/.1,f/.(len f) by A5,A14,A15,JORDAN5C:23; then LE f/.i,f/.(kk+1),L~f,f/.1,f/.(len f) by A154, JORDAN5C:13; then f/.i in LSeg(f/.kk,f/.(kk+1)) by A155,A157; then LSeg(f/.kk,f/.(kk+1)) /\ LSeg(f/.i,f/.(i+1))<>{} by A158 ,XBOOLE_0:def 4; then A159: not LSeg(f/.kk,f/.(kk+1)) misses LSeg (f/.i,f/.(i+1) ) by XBOOLE_0:def 7; A160: kk-1=kk-'1 by A131,XREAL_0:def 2; A161: now assume A162: i=kk-'1+2; then kk+1 =kk by A159,A164,TOPREAL1:def 7; then A166: i+1-1>=kk-1 by XREAL_1:9; kk+1>=i by A159,A165,A164,TOPREAL1:def 7; then A167: i=kk-'1+0 or ... or i=kk-'1+2 by A160,A166,NAT_1:62; A168: now per cases by A160,A167,A161; case i=kk; hence p44 in LSeg(f,kk) by A119,RLTOPSP1:68; end; case i=kk-1; hence p44 in LSeg(f,kk) by A132,RLTOPSP1:68; end; end; f is special by A5,TOPREAL1:def 8; then (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A127,A128,TOPREAL1:def 5; hence contradiction by A5,A6,A7,A8,A118,A121,A123,A124,A126 ,A127,A133,A151,A168,Th7; end; then i+1+k2=i+1+(kk-(i+1)) by XREAL_0:def 2 .=kk; then P[k2] by A127,A133,A151,FINSEQ_4:15; then A169: k2>=k by A27; kk-'(i+1)=kk-(i+1) by A156,XREAL_0:def 2; then kk-(i+1)+(i+1)>=k+(i+1) by A169,XREAL_1:7; then A170: LE f/.(i+1+k),f/.(kk),L~f,f/.1,f/.(len f) by A5,A30,A133, JORDAN5C:24; LE f/.(kk),f/.(i+1+k),L~f,f/.1,f/.(len f) by A6,A7,A8,A32,A122 ,A130,JORDAN5C:13; hence contradiction by A1,A6,A7,A8,A32,A108,A151,A170, JORDAN5C:12,TOPREAL4:2; end; end; hence contradiction; end; A171: p44 in LSeg(p,f/.(i+1)) by RLTOPSP1:68; A172: for p5 being Point of TOP-REAL 2 st LE p,p5,P,p1,p2 & LE p5, p44,P,p1,p2 holds p5`1>=e proof let p5 be Point of TOP-REAL 2; A173: Segment(P,p1,p2,p,p44)={p8 where p8 is Point of TOP-REAL 2: LE p,p8,P,p1,p2 & LE p8,p44,P,p1,p2} by JORDAN6:26; assume LE p,p5,P,p1,p2 & LE p5,p44,P,p1,p2; then A174: p5 in Segment(P,p1,p2,p,p44) by A173; p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68; then LSeg(p,p44) c= LSeg(f,i) by A11,A13,A119,TOPREAL1:6; then A175: LSeg(p,p44) c= P by A6,A19,A13; now per cases; case p44<>p; then LSeg(p,p44) is_an_arc_of p,p44 by TOPREAL1:9; then Segment(P,p1,p2,p,p44)=LSeg(p,p44) by A9,A5,A6,A7,A8,A11 ,A13,A14,A23,A171,A175,Th25,SPRECT_4:4; hence thesis by A4,A118,A174,TOPREAL1:3; end; case p44=p; then Segment(P,p1,p2,p,p44)={p44} by A1,A3,Th1,TOPREAL4:2; hence thesis by A118,A174,TARSKI:def 1; end; end; hence thesis; end; i+1<=i+1+k by NAT_1:11; then A176: LE p44,pk,P,p1,p2 by A5,A6,A7,A8,A17,A28,A32,JORDAN5C:24; then A177: p44 in P by JORDAN5C:def 3; A178: for p5 being Point of TOP-REAL 2 st LE p5,pk,P,p1,p2 & LE p,p5 ,P,p1,p2 holds p5`1>=e proof let p5 be Point of TOP-REAL 2; assume that A179: LE p5,pk,P,p1,p2 and A180: LE p,p5,P,p1,p2; A181: p5 in P by A179,JORDAN5C:def 3; now per cases by A1,A177,A181,Th19,TOPREAL4:2; case LE p44,p5,P,p1,p2; hence thesis by A120,A179; end; case LE p5,p44,P,p1,p2; hence thesis by A172,A180; end; end; hence thesis; end; LE p,p44,P,p1,p2 by A5,A6,A7,A8,A11,A13,A14,A23,A171,SPRECT_4:4; then LE p,pk,P,p1,p2 by A176,JORDAN5C:13; hence thesis by A3,A4,A9,A108,A178; end; end; hence thesis; end; end; hence thesis; end;