Copyright (c) 1998 Association of Mizar Users
environ vocabulary PRE_TOPC, EUCLID, ARYTM_1, COMPTS_1, TOPREAL2, PSCOMP_1, JORDAN6, TOPREAL1, JORDAN3, BOOLE, BORSUK_1, RELAT_1, TOPS_2, ORDINAL2, FUNCT_1, SUBSET_1, RCOMP_1, FINSEQ_1, TBSP_1, GOBRD10, FINSEQ_4; notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, REAL_1, NAT_1, RCOMP_1, RELAT_1, BINARITH, FINSEQ_1, FUNCT_1, FUNCT_2, FINSEQ_4, TOPREAL1, TOPREAL2, TBSP_1, GOBOARD1, GOBRD10, PRE_TOPC, TOPS_2, STRUCT_0, COMPTS_1, EUCLID, JORDAN3, PSCOMP_1, JORDAN5C, JORDAN6, TOPMETR; constructors RCOMP_1, GOBRD10, BINARITH, TOPREAL2, TOPS_2, TBSP_1, REAL_1, PSCOMP_1, JORDAN3, JORDAN4, JORDAN5C, JORDAN6, FINSEQ_4, GOBOARD1, T_0TOPSP, URYSOHN1, YELLOW_8; clusters STRUCT_0, RELSET_1, EUCLID, PSCOMP_1, PRE_TOPC, XREAL_0, ARYTM_3, GOBOARD1, BORSUK_2, MEMBERED; requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM; definitions TARSKI, XBOOLE_0, FUNCT_1; theorems TARSKI, JORDAN6, TOPREAL1, TOPREAL5, JORDAN5C, UNIFORM1, PRE_TOPC, FUNCT_2, TOPS_2, RELAT_1, FUNCT_1, SCMFSA_7, FINSEQ_1, AXIOMS, TOPMETR, FINSEQ_2, JORDAN3, GOBOARD1, BINARITH, NAT_1, REAL_1, RCOMP_1, FINSEQ_4, SQUARE_1, GOBRD10, SPRECT_1, XBOOLE_0, XBOOLE_1, FINSEQ_3, BORSUK_1, COMPTS_1, RELSET_1, AMI_5, JORDAN5B, XCMPLX_0, PARTFUN2, XCMPLX_1; schemes DOMAIN_1, NAT_1; begin :: Definition of the Segment and its property reserve p,p1,p2,p3,q for Point of TOP-REAL 2; Lm1: 0 < 1; Lm2: 2-'1 = 2-1 by SCMFSA_7:3 .=1; Lm3: for i, j, k be Nat holds i-'k <= j implies i <= j + k proof let i, j, k be Nat; assume A1: i-'k <= j; per cases; suppose A2: i >= k; i-'k +k <= j + k by A1,AXIOMS:24; hence i <= j + k by A2,AMI_5:4; suppose A3: i <= k; k <= j + k by NAT_1:29; hence i <= j + k by A3,AXIOMS:22; end; Lm4: for i, j, k be Nat holds j + k <= i implies k <= i -' j proof let i, j, k be Nat; assume A1: j + k <= i; per cases by A1,AXIOMS:21; suppose j + k = i; hence k <= i -' j by BINARITH:39; suppose j + k < i; hence k <= i -' j by Lm3; end; theorem Th1: for P being compact non empty Subset of TOP-REAL 2 st P is_simple_closed_curve holds W-min(P) in Lower_Arc(P) & E-max(P) in Lower_Arc(P) & W-min(P) in Upper_Arc(P) & E-max(P) in Upper_Arc(P) proof let P be compact non empty Subset of TOP-REAL 2; assume P is_simple_closed_curve; then Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) & Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by JORDAN6:65; hence thesis by TOPREAL1:4; end; theorem Th2: for P being compact non empty Subset of TOP-REAL 2,q st P is_simple_closed_curve & LE q,W-min(P),P holds q=W-min(P) proof let P be compact non empty Subset of TOP-REAL 2,q; assume A1:P is_simple_closed_curve & LE q,W-min(P),P; then A2:q in Upper_Arc(P) & W-min(P) in Upper_Arc(P) & LE q,W-min(P),Upper_Arc(P),W-min(P),E-max(P) by JORDAN6:def 10; Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8; hence q=W-min(P) by A2,JORDAN6:69; end; theorem Th3: for P being compact non empty Subset of TOP-REAL 2,q st P is_simple_closed_curve & q in P holds LE W-min(P),q,P proof let P be compact non empty Subset of TOP-REAL 2,q; assume A1: P is_simple_closed_curve & q in P; then A2:q in Upper_Arc(P) \/ Lower_Arc(P) by JORDAN6:65; A3: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) & Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,JORDAN6:65; A4: W-min(P) in Upper_Arc(P) by A1,Th1; now per cases by A2,XBOOLE_0:def 2; case A5:q in Upper_Arc(P); then LE W-min(P),q,Upper_Arc(P),W-min(P),E-max(P) by A3,JORDAN5C:10; hence LE W-min(P),q,P by A4,A5,JORDAN6:def 10; case A6:q in Lower_Arc(P); now per cases; case not q=W-min(P); hence LE W-min(P),q,P by A4,A6,JORDAN6:def 10; case A7: q=W-min(P); then LE W-min(P),q,Upper_Arc(P),W-min(P),E-max(P) by A3,A4,JORDAN5C:9; hence LE W-min(P),q,P by A4,A7,JORDAN6:def 10; end; hence LE W-min(P),q,P; end; hence LE W-min(P),q,P; end; definition let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2; func Segment(q1,q2,P) -> Subset of TOP-REAL 2 equals :Def1: {p: LE q1,p,P & LE p,q2,P} if q2<>W-min(P) otherwise {p1: LE q1,p1,P or q1 in P & p1=W-min(P)}; correctness proof ex B being Subset of TOP-REAL 2 st (q2<>W-min(P) implies B={p: LE q1,p,P & LE p,q2,P})& (not q2<>W-min(P) implies B={p1: LE q1,p1,P or q1 in P & p1=W-min(P)}) proof now per cases; case A1:q2<>W-min(P); defpred P[Point of TOP-REAL 2] means LE q1,$1,P & LE $1,q2,P; {p: P[p]} is Subset of TOP-REAL 2 from SubsetD; then reconsider C = {p: LE q1,p,P & LE p,q2,P} as Subset of TOP-REAL 2; (q2<>W-min(P) implies C={p: LE q1,p,P & LE p,q2,P})& (not q2<>W-min(P) implies C={p1: LE q1,p1,P or q1 in P & p1=W-min(P)}) by A1; hence thesis; case A2: not q2<>W-min(P); defpred P[Point of TOP-REAL 2] means LE q1,$1,P or q1 in P & $1=W-min(P); {p1: P[p1]} is Subset of TOP-REAL 2 from SubsetD; then reconsider C = {p1: LE q1,p1,P or q1 in P & p1=W-min(P)} as Subset of TOP-REAL 2; (q2<>W-min(P) implies C={p: LE q1,p,P & LE p,q2,P})& (not q2<>W-min(P) implies C={p1: LE q1,p1,P or q1 in P & p1=W-min(P)}) by A2; hence thesis; end; hence thesis; end; hence thesis; end; end; theorem for P being compact non empty Subset of TOP-REAL 2 st P is_simple_closed_curve holds Segment(W-min(P),E-max(P),P)=Upper_Arc(P) & Segment(E-max(P),W-min(P),P)=Lower_Arc(P) proof let P be compact non empty Subset of TOP-REAL 2; assume A1:P is_simple_closed_curve; then A2:E-max(P)<>W-min(P) by TOPREAL5:25; A3: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8; A4:{p: LE W-min(P),p,P & LE p,E-max(P),P} = Upper_Arc(P) proof A5: {p: LE W-min(P),p,P & LE p,E-max(P),P} c= Upper_Arc(P) proof let x be set;assume x in {p: LE W-min(P),p,P & LE p,E-max(P),P}; then consider p such that A6: p=x & ( LE W-min(P),p,P & LE p,E-max(P),P); now per cases by A6,JORDAN6:def 10; case p in Upper_Arc(P) & E-max(P) in Lower_Arc(P) & not E-max(P)=W-min(P); hence x in Upper_Arc(P) by A6; case p in Upper_Arc(P) & E-max(P) in Upper_Arc(P) & LE p,E-max(P),Upper_Arc(P),W-min(P),E-max(P); hence x in Upper_Arc(P) by A6; case A7: p in Lower_Arc(P) & E-max(P) in Lower_Arc(P) & not E-max(P)=W-min(P) & LE p,E-max(P),Lower_Arc(P),E-max(P),W-min(P); Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,JORDAN6:def 9; then p=E-max(P) by A7,JORDAN6:69; hence x in Upper_Arc(P) by A3,A6,TOPREAL1:4; end; hence x in Upper_Arc(P); end; Upper_Arc(P) c= {p: LE W-min(P),p,P & LE p,E-max(P),P} proof let x be set;assume A8: x in Upper_Arc(P); then reconsider p2=x as Point of TOP-REAL 2; A9: W-min(P) in Lower_Arc(P) & E-max(P) in Lower_Arc(P) & W-min(P) in Upper_Arc(P) & E-max(P) in Upper_Arc(P) by A1,Th1; LE W-min(P),p2,Upper_Arc(P),W-min(P),E-max(P) by A3,A8,JORDAN5C:10; then A10: LE W-min(P),p2,P by A8,A9,JORDAN6:def 10; LE p2,E-max(P),P by A2,A8,A9,JORDAN6:def 10; hence x in {p: LE W-min(P),p,P & LE p,E-max(P),P} by A10; end; hence thesis by A5,XBOOLE_0:def 10; end; {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)} = Lower_Arc(P) proof A11: {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)} c= Lower_Arc(P) proof let x be set;assume x in {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)}; then consider p1 such that A12: p1=x & (LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)); now per cases by A12; case A13: LE E-max(P),p1,P; now per cases by A12,A13,JORDAN6:def 10; case x in Lower_Arc(P); hence x in Lower_Arc(P); case A14: E-max(P) in Upper_Arc(P) & p1 in Upper_Arc(P) & LE E-max(P),p1,Upper_Arc(P),W-min(P),E-max(P); A15:Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:65; then LE p1,E-max(P),Upper_Arc(P),W-min(P),E-max(P) by A14,JORDAN5C:10; then A16:p1=E-max(P) by A14,A15,JORDAN5C:12; Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,JORDAN6:def 9; hence x in Lower_Arc(P) by A12,A16,TOPREAL1:4; end; hence x in Lower_Arc(P); case E-max(P) in P & p1=W-min(P); then x in {W-min(P),E-max(P)} by A12,TARSKI:def 2; then x in Upper_Arc(P) /\ Lower_Arc(P) by A1,JORDAN6:def 9; hence x in Lower_Arc(P) by XBOOLE_0:def 3; end; hence x in Lower_Arc(P); end; Lower_Arc(P) c= {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)} proof let x be set;assume A17: x in Lower_Arc(P); then reconsider p2=x as Point of TOP-REAL 2; Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:65; then not (E-max P in P & p2=W-min P) implies E-max P in Upper_Arc P & p2 in Lower_Arc P & not p2=W-min P by A17,SPRECT_1:16,TOPREAL1:4; then LE E-max(P),p2,P or E-max P in P & p2=W-min P by JORDAN6:def 10; hence x in {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)}; end; hence thesis by A11,XBOOLE_0:def 10; end; hence thesis by A2,A4,Def1; end; theorem Th5: for P being compact non empty Subset of TOP-REAL 2, q1,q2 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P holds q1 in P & q2 in P proof let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2; assume A1: P is_simple_closed_curve & LE q1,q2,P; then A2: Upper_Arc(P) \/ Lower_Arc(P)=P by JORDAN6:65; now per cases by A1,JORDAN6:def 10; case q1 in Upper_Arc(P) & q2 in Lower_Arc(P); hence q1 in P & q2 in P by A2,XBOOLE_0:def 2; case q1 in Upper_Arc(P) & q2 in Upper_Arc(P); hence q1 in P & q2 in P by A2,XBOOLE_0:def 2; case q1 in Lower_Arc(P) & q2 in Lower_Arc(P); hence q1 in P & q2 in P by A2,XBOOLE_0:def 2; end; hence thesis; end; theorem Th6: for P being compact non empty Subset of TOP-REAL 2, q1,q2 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P holds q1 in Segment(q1,q2,P) & q2 in Segment(q1,q2,P) proof let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2; assume A1: P is_simple_closed_curve & LE q1,q2,P; hereby per cases; suppose A2: q2<>W-min(P); q1 in P by A1,Th5; then LE q1,q1,P by A1,JORDAN6:71; then q1 in {p: LE q1,p,P & LE p,q2,P} by A1; hence q1 in Segment(q1,q2,P) by A2,Def1; suppose A3: q2=W-min(P); q1 in P by A1,Th5; then LE q1,q1,P by A1,JORDAN6:71; then q1 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)}; hence q1 in Segment(q1,q2,P) by A3,Def1; end; per cases; suppose A4: q2<>W-min(P); q2 in P by A1,Th5; then LE q2,q2,P by A1,JORDAN6:71; then q2 in {p: LE q1,p,P & LE p,q2,P} by A1; hence q2 in Segment(q1,q2,P) by A4,Def1; suppose A5: q2=W-min(P); q2 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)} by A1; hence q2 in Segment(q1,q2,P) by A5,Def1; end; theorem Th7: for P being compact non empty Subset of TOP-REAL 2, q1 being Point of TOP-REAL 2 st q1 in P & P is_simple_closed_curve holds q1 in Segment(q1,W-min P,P) proof let P be compact non empty Subset of TOP-REAL 2, q1 be Point of TOP-REAL 2 such that A1: q1 in P; assume P is_simple_closed_curve; then LE q1,q1,P by A1,JORDAN6:71; then q1 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)}; hence q1 in Segment(q1,W-min P,P) by Def1; end; theorem for P being compact non empty Subset of TOP-REAL 2, q being Point of TOP-REAL 2 st P is_simple_closed_curve & q in P & q<>W-min(P) holds Segment(q,q,P)={q} proof let P be compact non empty Subset of TOP-REAL 2, q be Point of TOP-REAL 2; assume that A1:P is_simple_closed_curve and A2: q in P and A3: q <> W-min P; for x being set holds x in Segment(q,q,P) iff x=q proof let x be set; hereby assume x in Segment(q,q,P); then x in {p: LE q,p,P & LE p,q,P} by A3,Def1; then ex p st p=x & (LE q,p,P & LE p,q,P); hence x=q by A1,JORDAN6:72; end; assume A4:x=q; LE q,q,P by A1,A2,JORDAN6:71; then x in {p: LE q,p,P & LE p,q,P} by A4; hence x in Segment(q,q,P) by A3,Def1; end; hence thesis by TARSKI:def 1; end; theorem for P being compact non empty Subset of TOP-REAL 2, q1,q2 being Point of TOP-REAL 2 st P is_simple_closed_curve & q1<>W-min(P) & q2<>W-min(P) holds not W-min(P) in Segment(q1,q2,P) proof let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2; assume A1: P is_simple_closed_curve & q1<>W-min(P) & q2<>W-min(P); then A2:Segment(q1,q2,P)={p: LE q1,p,P & LE p,q2,P} by Def1; now assume W-min(P) in Segment(q1,q2,P); then consider p such that A3: p=W-min(P) &(LE q1,p,P & LE p,q2,P) by A2; A4: q1 in Upper_Arc(P) & p in Upper_Arc(P) & LE q1,p,Upper_Arc(P),W-min(P),E-max(P) by A3,JORDAN6:def 10; Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8; hence contradiction by A1,A3,A4,JORDAN6:69; end; hence thesis; end; theorem Th10: for P being compact non empty Subset of TOP-REAL 2, q1,q2,q3 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & not(q1=q2 & q1=W-min(P)) & q1<>q3 & not(q2=q3 & q2=W-min(P)) holds Segment(q1,q2,P)/\ Segment(q2,q3,P)={q2} proof let P be compact non empty Subset of TOP-REAL 2, q1,q2,q3 be Point of TOP-REAL 2; assume A1: P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & not(q1=q2 & q1=W-min(P)) & q1<>q3 & not(q2=q3 & q2=W-min(P)); then A2: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by JORDAN6:def 8; thus Segment(q1,q2,P)/\ Segment(q2,q3,P) c= {q2} proof let x be set; assume x in Segment(q1,q2,P)/\ Segment(q2,q3,P); then A3: x in Segment(q1,q2,P) & x in Segment(q2,q3,P) by XBOOLE_0:def 3 ; now per cases; case q3<>W-min(P); then x in {p: LE q2,p,P & LE p,q3,P} by A3,Def1; then consider p such that A4: p=x & (LE q2,p,P & LE p,q3,P); now per cases; case q2<>W-min(P); then x in {p2: LE q1,p2,P & LE p2,q2,P} by A3,Def1; then ex p2 st p2=x & (LE q1,p2,P & LE p2,q2,P); hence x=q2 by A1,A4,JORDAN6:72; case A5:q2=W-min(P); then q1 in Upper_Arc(P) & q2 in Upper_Arc(P) & LE q1,q2,Upper_Arc(P),W-min(P),E-max(P) by A1,JORDAN6:def 10; hence contradiction by A1,A2,A5,JORDAN6:69; end; hence x=q2; case A6: q3=W-min(P); then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by A3,Def1; then consider p1 such that A7:p1=x &(LE q2,p1,P or q2 in P & p1=W-min(P)); p1 in {p: LE q1,p,P & LE p,q2,P} by A1,A3,A6,A7,Def1; then ex p st p=p1 & LE q1,p,P & LE p,q2,P; hence x=q2 by A1,A6,A7,JORDAN6:72; end; hence x in {q2} by TARSKI:def 1; end; let x be set;assume x in {q2}; then A8: x=q2 by TARSKI:def 1; then A9: x in Segment(q1,q2,P) by A1,Th6; x in Segment(q2,q3,P) by A1,A8,Th6; hence thesis by A9,XBOOLE_0:def 3; end; theorem Th11: for P being compact non empty Subset of TOP-REAL 2, q1,q2 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P & q1 <> W-min P & q2 <> W-min P holds Segment(q1,q2,P)/\ Segment(q2,W-min P,P)={q2} proof let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2; set q3 = W-min P; assume A1: P is_simple_closed_curve & LE q1,q2,P & q1<>q3 & not(q2=W-min(P)); thus Segment(q1,q2,P)/\ Segment(q2,W-min P,P) c= {q2} proof let x be set; assume x in Segment(q1,q2,P)/\ Segment(q2,q3,P); then A2: x in Segment(q1,q2,P) & x in Segment(q2,q3,P) by XBOOLE_0:def 3 ; then x in {p1: LE q2,p1,P or q2 in P & p1=W-min P} by Def1; then consider p1 such that A3:p1=x and A4: LE q2,p1,P or q2 in P & p1=W-min P; p1 in {p: LE q1,p,P & LE p,q2,P} by A1,A2,A3,Def1; then A5: ex p st p=p1 & LE q1,p,P & LE p,q2,P; per cases by A4; suppose LE q2,p1,P; then x=q2 by A1,A3,A5,JORDAN6:72; hence x in {q2} by TARSKI:def 1; suppose q2 in P & p1=W-min(P); hence x in {q2} by A1,A5,Th2; end; let x be set;assume x in {q2}; then A6: x=q2 by TARSKI:def 1; then A7: x in Segment(q1,q2,P) by A1,Th6; q2 in P by A1,Th5; then x in Segment(q2,q3,P) by A1,A6,Th7; hence thesis by A7,XBOOLE_0:def 3; end; theorem Th12: for P being compact non empty Subset of TOP-REAL 2, q1,q2 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P & q1<>q2 & q1<>W-min(P) holds Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P)={W-min(P)} proof let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2; assume A1: P is_simple_closed_curve & LE q1,q2,P & q1<>q2 & q1<>W-min(P); then A2: q1 in P & q2 in P by Th5; thus Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P) c= {W-min(P)} proof let x be set; assume x in Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P); then A3: x in Segment(q2,W-min(P),P) & x in Segment(W-min(P),q1,P) by XBOOLE_0:def 3; then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by Def1; then consider p1 such that A4: p1=x &(LE q2,p1,P or q2 in P & p1=W-min(P) ); now per cases by A4; case A5:LE q2,p1,P; x in {p: LE W-min(P),p,P & LE p,q1,P} by A1,A3,Def1; then ex p2 st p2=x & LE W-min(P),p2,P & LE p2,q1,P; then LE q2,q1,P by A1,A4,A5,JORDAN6:73; hence contradiction by A1,JORDAN6:72; case q2 in P & p1=W-min(P); hence x=W-min(P) by A4; end; hence x in {W-min(P)} by TARSKI:def 1; end; let x be set;assume x in {W-min(P)}; then A6: x=W-min(P) by TARSKI:def 1; then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by A2; then A7: x in Segment(q2,W-min(P),P) by Def1; LE W-min(P),q1,P by A1,A2,Th3; then x in Segment(W-min(P),q1,P) by A1,A6,Th6; hence thesis by A7,XBOOLE_0:def 3; end; theorem Th13: for P being compact non empty Subset of TOP-REAL 2, q1,q2,q3,q4 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P & q1<>q2 & q2<>q3 holds Segment(q1,q2,P) misses Segment(q3,q4,P) proof let P be compact non empty Subset of TOP-REAL 2, q1,q2,q3,q4 be Point of TOP-REAL 2; assume that A1:P is_simple_closed_curve and A2: LE q1,q2,P and A3: LE q2,q3,P and A4: LE q3,q4,P and A5: q1<>q2 and A6: q2<>q3; assume A7:Segment(q1,q2,P)/\ Segment(q3,q4,P)<>{}; consider x being Element of Segment(q1,q2,P)/\ Segment(q3,q4,P); A8:x in Segment(q1,q2,P) & x in Segment(q3,q4,P) by A7,XBOOLE_0:def 3; now per cases; case q4=W-min(P); then q3=W-min(P) by A1,A4,Th2; hence contradiction by A1,A3,A6,Th2; case q4<>W-min(P); then x in {p1: LE q3,p1,P & LE p1,q4,P} by A8,Def1; then consider p1 such that A9:p1=x &(LE q3,p1,P & LE p1,q4,P); q2<>W-min(P) by A1,A2,A5,Th2; then x in {p2: LE q1,p2,P & LE p2,q2,P} by A8,Def1; then consider p2 such that A10:p2=x &(LE q1,p2,P & LE p2,q2,P); LE q3,q2,P by A1,A9,A10,JORDAN6:73; hence contradiction by A1,A3,A6,JORDAN6:72; end; hence contradiction; end; theorem Th14: for P being compact non empty Subset of TOP-REAL 2, q1,q2,q3 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & q1<>W-min P & q1<>q2 & q2<>q3 holds Segment(q1,q2,P) misses Segment(q3,W-min P,P) proof let P be compact non empty Subset of TOP-REAL 2, q1,q2,q3 be Point of TOP-REAL 2; assume A1:P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & q1<>W-min P & q1<>q2 & q2<>q3; assume A2:Segment(q1,q2,P)/\ Segment(q3,W-min P,P)<>{}; consider x being Element of Segment(q1,q2,P)/\ Segment(q3,W-min P,P); A3:x in Segment(q1,q2,P) & x in Segment(q3,W-min P,P) by A2,XBOOLE_0:def 3; then x in {p1: LE q3,p1,P or q3 in P & p1=W-min P} by Def1; then consider p1 such that A4: p1=x and A5: LE q3,p1,P or q3 in P & p1=W-min P; q2 <> W-min P by A1,Th2; then x in {p: LE q1,p,P & LE p,q2,P} by A3,Def1; then ex p3 st p3 = x & LE q1,p3,P & LE p3,q2,P; then LE q3,q2,P by A1,A4,A5,Th2,JORDAN6:73; hence contradiction by A1,JORDAN6:72; end; begin :: A function to divide the simple closed curve reserve n for Nat; theorem Th15: for P being non empty Subset of TOP-REAL n, f being map of I[01], (TOP-REAL n)|P st P<>{} & f is_homeomorphism ex g being map of I[01],TOP-REAL n st f=g & g is continuous & g is one-to-one proof let P be non empty Subset of TOP-REAL n, f be map of I[01], (TOP-REAL n)|P; assume A1: P<>{} & f is_homeomorphism; the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P) by PRE_TOPC:12 .=P by PRE_TOPC:def 10; then f is Function of the carrier of I[01],the carrier of TOP-REAL n by FUNCT_2:9; then reconsider g1=f as map of I[01],TOP-REAL n; A2:the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P) by PRE_TOPC:12; A3:[#]((TOP-REAL n)|P)= P by PRE_TOPC:def 10; A4:f is one-to-one & f is continuous & f" is continuous by A1,TOPS_2:def 5; for P2 being Subset of TOP-REAL n st P2 is open holds g1"P2 is open proof let P2 be Subset of TOP-REAL n; assume A5: P2 is open; P2 /\ P is Subset of (TOP-REAL n)|P by A2,A3,XBOOLE_1:17; then reconsider B1=P2 /\ P as Subset of (TOP-REAL n)|P; B1 is open by A3,A5,TOPS_2:32; then A6:f"B1 is open by A4,TOPS_2:55; A7:f"B1 = f"P2 /\ f"P by FUNCT_1:137; f"(rng f) c= f"P by A2,A3,RELAT_1:178; then A8:dom f c= f"P by RELAT_1:169; f"P c= dom f by RELAT_1:167; then A9:f"P=dom f by A8,XBOOLE_0:def 10; f"P2 c= dom f by RELAT_1:167; hence g1"P2 is open by A6,A7,A9,XBOOLE_1:28; end; then g1 is continuous by TOPS_2:55; hence thesis by A4; end; theorem Th16: for P being non empty Subset of TOP-REAL n, g being map of I[01], (TOP-REAL n) st g is continuous one-to-one & rng g = P ex f being map of I[01],(TOP-REAL n)|P st f=g & f is_homeomorphism proof let P be non empty Subset of TOP-REAL n, g be map of I[01], (TOP-REAL n); assume that A1: g is continuous one-to-one and A2: rng g = P; the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P) by PRE_TOPC:12; then A3: the carrier of (TOP-REAL n)|P = P by PRE_TOPC:def 10; then g is Function of the carrier of I[01],the carrier of (TOP-REAL n)|P by A2,FUNCT_2:8; then reconsider f=g as map of I[01],(TOP-REAL n)|P; take f; thus f = g; A4: dom f = the carrier of I[01] by FUNCT_2:def 1 .= [#]I[01] by PRE_TOPC:12; A5: rng f = [#]((TOP-REAL n)|P) by A2,PRE_TOPC:def 10; A6: [#]((TOP-REAL n)|P)= P by PRE_TOPC:def 10; for P2 being Subset of (TOP-REAL n)|P st P2 is open holds f"P2 is open proof let P2 be Subset of (TOP-REAL n)|P; assume A7: P2 is open; consider C being Subset of TOP-REAL n such that A8: C is open and A9: C /\ [#]((TOP-REAL n)|P) = P2 by A7,TOPS_2:32; A10: f"C c= [#]I[01] by PRE_TOPC:14; g"P = [#]I[01] by A3,A4,RELSET_1:38; then f"P2 = f"C /\ [#]I[01] by A6,A9,FUNCT_1:137 .= f"C by A10,XBOOLE_1:28; hence f"P2 is open by A1,A8,TOPS_2:55; end; then A11: f is continuous by TOPS_2:55; (TOP-REAL n)|P is_T2 by TOPMETR:3; hence thesis by A1,A4,A5,A11,COMPTS_1:26; end; definition cluster increasing -> one-to-one FinSequence of REAL; coherence proof let f be FinSequence of REAL; assume A1:f is increasing; let x,y be set;assume A2: x in dom f & y in dom f & f.x=f.y; then reconsider nx=x,ny=y as Nat; A3: nx<=ny by A1,A2,GOBOARD1:def 1; nx>=ny by A1,A2,GOBOARD1:def 1; hence x=y by A3,REAL_1:def 5; end; end; theorem Th17: for f being FinSequence of REAL st f is increasing holds f is one-to-one proof let f be FinSequence of REAL; assume f is increasing; then reconsider f as increasing FinSequence of REAL; f is one-to-one; hence thesis; end; Lm5: now let h2 be Nat; h2<h2+1 by NAT_1:38; then h2-1<h2+1-1 by REAL_1:54; then h2-1<h2 by XCMPLX_1:26; then h2-1-1<h2-1 & h2-1<h2 by REAL_1:54; hence h2-1-1<h2 by AXIOMS:22; end; Lm6: 0 in [.0,1.] & 1 in [.0,1.] by RCOMP_1:15; theorem Th18: for A being Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st A is_an_arc_of p1,p2 ex g being map of I[01], TOP-REAL 2 st g is continuous one-to-one & rng g = A & g.0 = p1 & g.1 = p2 proof let A be Subset of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2; assume A1: A is_an_arc_of p1,p2; then reconsider A' = A as non empty Subset of TOP-REAL 2 by TOPREAL1:4; consider f being map of I[01], (TOP-REAL 2)|A' such that A2: f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2; A3: rng f=[#]((TOP-REAL 2)|A') by A2,TOPS_2:def 5; consider g being map of I[01], TOP-REAL 2 such that A4: f=g and A5: g is continuous one-to-one by A2,Th15; take g; thus g is continuous one-to-one by A5; thus rng g = A by A3,A4,PRE_TOPC:def 10; thus thesis by A2,A4; end; theorem Th19: for P being non empty Subset of TOP-REAL 2, p1, p2, q1, q2 being Point of TOP-REAL 2, g being map of I[01], TOP-REAL 2, s1, s2 being Real st P is_an_arc_of p1,p2 & g is continuous one-to-one & rng g = P & g.0 = p1 & g.1 = p2 & g.s1 = q1 & 0 <= s1 & s1 <= 1 & g.s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds LE q1,q2,P,p1,p2 proof let P be non empty Subset of TOP-REAL 2, p1, p2, q1, q2 be Point of TOP-REAL 2, g be map of I[01], TOP-REAL 2, s1, s2 be Real such that A1: P is_an_arc_of p1,p2 and A2: g is continuous one-to-one and A3: rng g = P; ex f being map of I[01],(TOP-REAL 2)|P st f=g & f is_homeomorphism by A2,A3,Th16; hence thesis by A1,JORDAN5C:8; end; theorem Th20: for P being non empty Subset of TOP-REAL 2, p1, p2, q1, q2 being Point of TOP-REAL 2, g being map of I[01], TOP-REAL 2, s1, s2 being Real st g is continuous one-to-one & rng g = P & g.0 = p1 & g.1 = p2 & g.s1 = q1 & 0 <= s1 & s1 <= 1 & g.s2 = q2 & 0 <= s2 & s2 <= 1 & LE q1,q2,P,p1,p2 holds s1 <= s2 proof let P be non empty Subset of TOP-REAL 2, p1, p2, q1, q2 be Point of TOP-REAL 2, g be map of I[01], TOP-REAL 2, s1, s2 be Real such that A1: g is continuous one-to-one and A2: rng g = P; ex f being map of I[01],(TOP-REAL 2)|P st f=g & f is_homeomorphism by A1,A2,Th16; hence thesis by JORDAN5C:def 3; end; theorem :: Dividing simple closed curve into segments. for P being compact non empty Subset of TOP-REAL 2, e being Real st P is_simple_closed_curve & e > 0 ex h being FinSequence of the carrier of TOP-REAL 2 st h.1=W-min(P) & h is one-to-one & 8<=len h & rng h c= P &(for i being Nat st 1<=i & i<len h holds LE h/.i,h/.(i+1),P) &(for i being Nat,W being Subset of Euclid 2 st 1<=i & i<len h & W=Segment(h/.i,h/.(i+1),P) holds diameter(W)<e) & (for W being Subset of Euclid 2 st W=Segment(h/.len h,h/.1,P) holds diameter(W)<e) & (for i being Nat st 1<=i & i+1<len h holds Segment(h/.i,h/.(i+1),P)/\ Segment(h/.(i+1),h/.(i+2),P)={h/.(i+1)}) & Segment(h/.len h,h/.1,P)/\ Segment(h/.1,h/.2,P)={h/.1} & Segment(h/.(len h-' 1),h/.len h,P)/\ Segment(h/.len h,h/.1,P)={h/.len h} & Segment(h/.(len h-'1),h/.len h,P) misses Segment(h/.1,h/.2,P) &(for i,j being Nat st 1<=i & i < j & j < len h & not(i,j are_adjacent1) holds Segment(h/.i,h/.(i+1),P) misses Segment(h/.j,h/.(j+1),P)) & (for i being Nat st 1 < i & i+1 < len h holds Segment(h/.len h,h/.1,P) misses Segment(h/.i,h/.(i+1),P)) proof let P be compact non empty Subset of TOP-REAL 2, e be Real; assume A1: P is_simple_closed_curve & e > 0; then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by JORDAN6:def 8; then consider g1 being map of I[01], TOP-REAL 2 such that A3: g1 is continuous one-to-one and A4: rng g1 = Upper_Arc P and A5: g1.0 = W-min P & g1.1 = E-max P by Th18; A6: dom g1 =[.0,1.] by BORSUK_1:83,FUNCT_2:def 1; A7: 0 in dom g1 & 1 in dom g1 by Lm6,BORSUK_1:83,FUNCT_2:def 1; A8: E-max P in Upper_Arc P & W-min P in Upper_Arc P by A1,Th1; consider h1 being FinSequence of REAL such that A9: h1.1=0 & h1.len h1=1 & 5<=len h1 & rng h1 c= the carrier of I[01] & h1 is increasing &(for i being Nat,Q being Subset of I[01], W being Subset of Euclid 2 st 1<=i & i<len h1 & Q=[.h1/.i,h1/.(i+1).] & W=g1.:Q holds diameter(W)<e) by A1,A3,A5,UNIFORM1:15; A10:h1 is one-to-one by A9,Th17; A11: Lower_Arc P is_an_arc_of E-max P, W-min P by A1,JORDAN6:def 9; then consider g2 being map of I[01], TOP-REAL 2 such that A12: g2 is continuous one-to-one and A13: rng g2 = Lower_Arc P and A14: g2.0 = E-max P & g2.1 = W-min P by Th18; A15: dom g2 = [.0,1.] by BORSUK_1:83,FUNCT_2:def 1; consider h2 being FinSequence of REAL such that A16: h2.1=0 & h2.len h2=1 & 5<=len h2 & rng h2 c= the carrier of I[01] & h2 is increasing &(for i being Nat,Q being Subset of I[01], W being Subset of Euclid 2 st 1<=i & i<len h2 & Q=[.h2/.i,h2/.(i+1).] & W=g2.:Q holds diameter(W)<e) by A1,A12,A14,UNIFORM1:15; A17: len h2-1-1<len h2 by Lm5; A18:h2 is one-to-one by A16,Th17; h1 is FinSequence of the carrier of I[01] by A9,FINSEQ_1:def 4; then reconsider h11=g1*h1 as FinSequence of the carrier of TOP-REAL 2 by FINSEQ_2:36; A19:rng h1 c= dom g1 by A9,FUNCT_2:def 1; then A20:dom h1=dom h11 by RELAT_1:46; then A21: len h1=len h11 by FINSEQ_3:31; h2 is FinSequence of the carrier of I[01] by A16,FINSEQ_1:def 4; then reconsider h21=g2*h2 as FinSequence of the carrier of TOP-REAL 2 by FINSEQ_2:36; dom g2=the carrier of I[01] by FUNCT_2:def 1; then A22:dom h2=dom h21 by A16,RELAT_1:46; then A23: len h2=len h21 by FINSEQ_3:31; A24: 1<=len h1 by A9,AXIOMS:22; then A25: 1 in dom h1 by FINSEQ_3:27; A26:len h1 in dom h1 by A24,FINSEQ_3:27; A27: 1<=len h2 by A16,AXIOMS:22; then A28:1 in dom h2 by FINSEQ_3:27; A29: len h2 in dom h2 by A27,FINSEQ_3:27; A30: h21.1=E-max P by A14,A16,A28,FUNCT_1:23; A31: h21.len h2=W-min P by A14,A16,A29,FUNCT_1:23; A32:1 in dom g2 by Lm6,BORSUK_1:83,FUNCT_2:def 1; A33:dom g1=[.0,1.] by BORSUK_1:83,FUNCT_2:def 1; then A34:1 in dom (g1*h1) by A9,A25,Lm6,FUNCT_1:21; A35:len h1 in dom h1 by A24,FINSEQ_3:27; h1.len h1 in dom g1 by A9,A33,TOPREAL5:1; then A36:len h1 in dom (g1*h1) by A26,FUNCT_1:21; then A37: h11.len h1=E-max(P) by A5,A9,FUNCT_1:22; reconsider h0=h11^(mid(h21,2,len h21-' 1)) as FinSequence of the carrier of TOP-REAL 2; A38: h11.1=W-min P by A5,A9,A34,FUNCT_1:22; take h0; thus A39: h0.1=W-min P by A34,A38,FINSEQ_1:def 7; A40:len h0=len h11+len (mid(h21,2,len h21 -'1)) by FINSEQ_1:35; 2<=len h21 by A16,A23,AXIOMS:22; then A41:1+1-1<=len h21-1 by REAL_1:49; then 0<=len h21-1 by AXIOMS:22; then A42:len h21-'1=len h21 -1 by BINARITH:def 3; len h21<=len h21 +1 by NAT_1:37; then len h21 -1<=len h21 +1-1 by REAL_1:49; then A43:2<=len h21 & 1<=len h21-'1 & len h21-'1<=len h21 by A16,A23,A41,A42,AXIOMS:22,XCMPLX_1:26; 3<len h21 by A16,A23,AXIOMS:22; then 2+1-1<len h21 -1 by REAL_1:54; then A44:2<len h21 -'1 by A41,JORDAN3:1; then A45:len h21 -'1-'2=len h21 -'1-2 by SCMFSA_7:3; A46:len (mid(h21,2,len h21 -'1)) =(len h21-'1)-'2+1 by A43,A44,JORDAN3:27; then A47:len h0=len h1+(len h2-2) by A21,A23,A40,A42,A45,XCMPLX_1:229; 3+2-2<=len h2 -2 by A16,REAL_1:49; then 1<=len h2 -2 by AXIOMS:22; then A48: len h1+1<=len h0 by A47,REAL_1:55; then A49: len h0>len h1 by NAT_1:38; then A50: 1<len h0 by A24,AXIOMS:22; then A51: len h0 in dom h0 by FINSEQ_3:27; then A52: h0/.len h0=h0.len h0 by FINSEQ_4:def 4; A53: 1<=len h0-len h1 by A48,REAL_1:84; A54: len h0-len h11=len h0-'len h11 by A21,A49,SCMFSA_7:3; then A55: 1<=len h0-'len h11 by A21,A48,REAL_1:84; A56: 2<len h1 by A9,AXIOMS:22; then A57:2 in dom h1 by FINSEQ_3:27; A58: 1+1<=len h0 by A49,A56,AXIOMS:22; then A59:2 in dom h0 by FINSEQ_3:27; A60:h0.2=h11.2 by A21,A56,SCMFSA_7:9; A61: 1 in dom h0 by A50,FINSEQ_3:27; then A62: h0/.1 = h0.1 by FINSEQ_4:def 4; A63: h0/.1=W-min(P) by A39,A61,FINSEQ_4:def 4; A64:h11 is one-to-one by A3,A10,FUNCT_1:46; A65:h21 is one-to-one by A12,A18,FUNCT_1:46; thus A66: h0 is one-to-one proof let x,y be set;assume A67: x in dom h0 & y in dom h0 & h0.x=h0.y; then reconsider nx=x,ny=y as Nat; A68:1<=nx & nx<=len h0 by A67,FINSEQ_3:27; A69:1<=ny & ny<=len h0 by A67,FINSEQ_3:27; now per cases; case nx<=len h1; then A70:nx in dom h1 by A68,FINSEQ_3:27; then A71: h1.nx in rng h1 by FUNCT_1:def 5; A72:h0.nx=h11.nx by A20,A70,FINSEQ_1:def 7 .=g1.(h1.nx) by A20,A70,FUNCT_1:22; then A73:h0.nx in Upper_Arc(P) by A4,A19,A71,FUNCT_1:def 5; now per cases; case ny<=len h1; then A74:ny in dom h1 by A69,FINSEQ_3:27; then A75: h1.ny in rng h1 by FUNCT_1:def 5; h0.ny=h11.ny by A20,A74,FINSEQ_1:def 7 .=g1.(h1.ny) by A74,FUNCT_1:23; then h1.nx=h1.ny by A3,A19,A67,A71,A72,A75,FUNCT_1:def 8; hence nx=ny by A10,A70,A74,FUNCT_1:def 8; case A76:ny>len h1; then A77:len h1 +1<=ny by NAT_1:38; A78:len h11+1<=ny & ny<=len h11 + len (mid(h21,2,len h21 -'1)) by A21,A69,A76,FINSEQ_1:35,NAT_1:38; then A79:h0.ny=(mid(h21,2,len h21 -'1)).(ny -len h11) by FINSEQ_1:36 ; A80:ny-len h11=ny-'len h11 by A21,A76,SCMFSA_7:3; A81: ny-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A78,REAL_1:49; len h1 +1-len h1<=ny-len h1 by A77,REAL_1:49; then A82:1<=ny-'len h11 & ny-'len h11<=len mid(h21,2,len h21 -'1) by A21,A80,A81,XCMPLX_1:26; then A83:h0.ny=h21.(ny-'len h11 +2-'1) by A43,A44,A79,A80,JORDAN3:27; 1+1<=ny-'len h11+1 by A82,AXIOMS:24; then 1+1<=ny-'len h11+1+1-1 by XCMPLX_1:26; then A84:2<=ny-'len h11+2-1 by XCMPLX_1:1; 0<=ny-'len h11 by NAT_1:18; then A85: 0+2<=ny-'len h11 +2 by AXIOMS:24; ny-len h11<=len h1+(len h2-2)-len h11 by A47,A69,REAL_1:49; then ny-len h11<=(len h2-2) by A21,XCMPLX_1:26; then ny-'len h11+2<=len h2-2+2 by A80,AXIOMS:24; then A86: ny-'len h11+2<=len h2 by XCMPLX_1:27; then A87:ny-'len h11+2-1<=len h2-1 by REAL_1:49; A88:1<=(ny-'len h11 +2-'1) & (ny-'len h11 +2-'1)<=len h21 by A23,A85,A86,Lm2,JORDAN3:5,7; then A89:(ny-'len h11 +2-'1) in dom h21 by FINSEQ_3:27; then h0.ny in rng h21 by A83,FUNCT_1:def 5; then h0.ny in rng g2 by FUNCT_1:25; then h0.nx in Upper_Arc(P)/\ Lower_Arc(P) by A13,A67,A73,XBOOLE_0:def 3; then A90: h0.nx in {W-min(P),E-max(P)} by A1,JORDAN6:65; A91:ny-'len h11+2-'1<=len h2-1 by A87,A88,JORDAN3:1; A92:2<=ny-'len h11+2-'1 by A84,A88,JORDAN3:1; now per cases by A90,TARSKI:def 2; case h0.nx=W-min(P); then h21.(ny-'len h11 +2-'1)=W-min(P) by A43,A44,A67,A79,A80,A82,JORDAN3:27; then len h21=(ny-'len h11 +2-'1) by A22,A23,A29,A31,A65,A89,FUNCT_1:def 8; then len h21+1<=len h21-1+1 by A23,A91,AXIOMS:24; then len h21+1<=len h21-(1-1) by XCMPLX_1:37; then len h21+1-len h21<=len h21 -len h21 by REAL_1:49; then len h21+1-len h21<=0 by XCMPLX_1:14; hence contradiction by Lm1,XCMPLX_1:26; case h0.nx=E-max(P); then 1=(ny-'len h11 +2-'1) by A22,A28,A30,A65,A67,A83,A89,FUNCT_1:def 8; hence contradiction by A92; end; hence nx=ny; end; hence nx=ny; case A93:nx>len h1; then A94:len h1 +1<=nx by NAT_1:38; A95:len h11+1<=nx & nx<=len h11 + len (mid(h21,2,len h21 -'1)) by A21,A68,A93,FINSEQ_1:35,NAT_1:38; then A96:h0.nx=(mid(h21,2,len h21 -'1)).(nx -len h11) by FINSEQ_1:36; A97:nx-len h11=nx-'len h11 by A21,A93,SCMFSA_7:3; A98: nx-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A95,REAL_1:49; len h1 +1-len h1<=nx-len h1 by A94,REAL_1:49; then A99:1<=nx-'len h11 & nx-'len h11<=len mid(h21,2,len h21 -'1) by A21,A97,A98,XCMPLX_1:26; then A100:h0.nx=h21.(nx-'len h11 +2-'1) by A43,A44,A96,A97,JORDAN3:27; 1+1<=nx-'len h11+1 by A99,AXIOMS:24; then 1+1<=nx-'len h11+1+1-1 by XCMPLX_1:26; then A101:2<=nx-'len h11+2-1 by XCMPLX_1:1; 0<=nx-'len h11 by NAT_1:18; then A102: 0+2<=nx-'len h11 +2 by AXIOMS:24; nx-len h11<=len h1+(len h2-2)-len h11 by A47,A68,REAL_1:49; then nx-len h11<=(len h2-2) by A21,XCMPLX_1:26; then nx-'len h11+2<=len h2-2+2 by A97,AXIOMS:24; then A103: nx-'len h11+2<=len h2 by XCMPLX_1:27; then A104:nx-'len h11+2-1<=len h2-1 by REAL_1:49; A105:1<=(nx-'len h11 +2-'1) & (nx-'len h11 +2-'1)<=len h21 by A23,A102,A103,Lm2,JORDAN3:5,7; then A106:(nx-'len h11 +2-'1) in dom h21 by FINSEQ_3:27; then h0.nx in rng h21 by A100,FUNCT_1:def 5; then A107:h0.nx in Lower_Arc(P) by A13,FUNCT_1:25; now per cases; case ny<=len h1; then A108:ny in dom h1 by A69,FINSEQ_3:27; then A109: h1.ny in rng h1 by FUNCT_1:def 5; h0.ny=h11.ny by A20,A108,FINSEQ_1:def 7 .=g1.(h1.ny) by A20,A108,FUNCT_1:22; then h0.ny in rng g1 by A19,A109,FUNCT_1:def 5; then h0.ny in Upper_Arc(P)/\ Lower_Arc(P) by A4,A67,A107,XBOOLE_0: def 3; then A110: h0.ny in {W-min(P),E-max(P)} by A1,JORDAN6:65; A111:nx-'len h11+2-'1<=len h2-1 by A104,A105,JORDAN3:1; A112:2<=nx-'len h11+2-'1 by A101,A105,JORDAN3:1; now per cases by A110,TARSKI:def 2; case h0.ny=W-min(P); then len h21=(nx-'len h11 +2-'1) by A22,A23,A29,A31,A65,A67,A100,A106,FUNCT_1:def 8; then len h21+1<=len h21-1+1 by A23,A111,AXIOMS:24; then len h21+1<=len h21-(1-1) by XCMPLX_1:37; then len h21+1-len h21<=len h21 -len h21 by REAL_1:49; then len h21+1-len h21<=0 by XCMPLX_1:14; hence contradiction by Lm1,XCMPLX_1:26; case h0.ny=E-max(P); then h21.(nx-'len h11 +2-'1)=E-max(P) by A43,A44,A67,A96,A97,A99,JORDAN3:27; then 1=(nx-'len h11 +2-'1) by A22,A28,A30,A65,A106,FUNCT_1:def 8; hence contradiction by A112; end; hence nx=ny; case A113:ny>len h1; then A114:len h1 +1<=ny by NAT_1:38; then A115:h0.ny=(mid(h21,2,len h21 -'1)).(ny -len h11) by A21,A40,A69,FINSEQ_1:36; A116:ny-len h11=ny-'len h11 by A21,A113,SCMFSA_7:3; ny-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A69,REAL_1:49; then A117:ny-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; len h1 +1-len h1<=ny-len h1 by A114,REAL_1:49; then 1<=ny-len h11 by A21,XCMPLX_1:26; then A118:h0.ny=h21.(ny-'len h11 +2-'1) by A43,A44,A115,A116,A117,JORDAN3:27; 0<=ny-'len h11 by NAT_1:18; then A119: 0+2<=ny-'len h11 +2 by AXIOMS:24; ny-len h11<=len h1+(len h2-2)-len h11 by A47,A69,REAL_1:49; then ny-len h11<=(len h2-2) by A21,XCMPLX_1:26; then ny-'len h11+2<=len h2-2+2 by A116,AXIOMS:24; then ny-'len h11+2<=len h2 by XCMPLX_1:27; then A120:1<=(ny-'len h11 +2-'1) & (ny-'len h11 +2-'1)<=len h21 by A23,A119,Lm2,JORDAN3:5,7; then (ny-'len h11 +2-'1) in dom h21 by FINSEQ_3:27; then nx-'len h1+2-'1=ny-'len h1+2-'1 by A21,A65,A67,A100,A106,A118,FUNCT_1:def 8; then nx-'len h1+2-1=ny-'len h1+2-'1 by A21,A105,JORDAN3:1; then nx-'len h1+2-1=ny-'len h1+2-1 by A21,A120,JORDAN3:1; then nx-'len h1+(2-1)=ny-'len h1+2-1 by XCMPLX_1:29; then nx-'len h1+(2-1)=ny-'len h1+(2-1) by XCMPLX_1:29; then nx-'len h1=ny-'len h1+(2-1)-(2-1) by XCMPLX_1:26; then nx-len h1=ny-len h1 by A21,A97,A116,XCMPLX_1:26; then len h1+nx-len h1=len h1+(ny-len h1) by XCMPLX_1:29; then nx=len h1+(ny-len h1) by XCMPLX_1:26; then nx=len h1+ny-len h1 by XCMPLX_1:29; hence nx=ny by XCMPLX_1:26; end; hence nx=ny; end; hence x=y; end; then A121: h0/.len h0 <> W-min P by A24,A39,A49,A51,A52,A61,FUNCT_1:def 8; 3+2-2<=len h2 -2 by A16,REAL_1:49; then 5+3<=len h1+(len h2 -2) by A9,REAL_1:55; hence A122: 8<=len h0 by A21,A23,A40,A42,A45,A46,XCMPLX_1:229; A123:rng (g1*h1) c= rng g1 by RELAT_1:45; A124:rng (mid(h21,2,len h21 -'1)) c= rng h21 by JORDAN3:28; rng (g2*h2) c= rng g2 by RELAT_1:45; then rng (mid(h21,2,len h21 -'1)) c= rng g2 by A124,XBOOLE_1:1; then rng h11 \/ rng (mid(h21,2,len h21 -'1)) c= Upper_Arc(P) \/ Lower_Arc(P) by A4,A13,A123,XBOOLE_1:13; then rng h0 c=Upper_Arc(P) \/ Lower_Arc(P) by FINSEQ_1:44; hence rng h0 c= P by A1,JORDAN6:def 9; thus for i being Nat st 1<=i & i<len h0 holds LE h0/.i,h0/.(i+1),P proof let i be Nat;assume A125: 1<=i & i<len h0; then A126:i+1<=len h0 by NAT_1:38; A127:1<i+1 by A125,NAT_1:38; A128:i<i+1 by NAT_1:38; now per cases; case A129:i<len h1; then A130:i+1<=len h1 by NAT_1:38; A131:h0.i=h11.i by A21,A125,A129,SCMFSA_7:9; A132:i in dom h1 by A125,A129,FINSEQ_3:27; then A133:h0.i=g1.(h1.i) by A131,FUNCT_1:23; A134: h1.i in rng h1 by A132,FUNCT_1:def 5; then A135:0<=h1.i & h1.i<=1 by A9,BORSUK_1:83,TOPREAL5:1; A136:h0.(i+1)=h11.(i+1) by A21,A127,A130,SCMFSA_7:9; A137:i+1 in dom h1 by A127,A130,FINSEQ_3:27; then A138:h0.(i+1)=g1.(h1.(i+1)) by A136,FUNCT_1:23; A139: h1.(i+1) in rng h1 by A137,FUNCT_1:def 5; then A140:0<=h1.(i+1) & h1.(i+1)<=1 by A9,BORSUK_1:83,TOPREAL5:1; A141:h1.i<h1.(i+1) by A9,A128,A132,A137,GOBOARD1:def 1; i in dom h0 by A125,FINSEQ_3:27; then A142:h0/.i=h0.i by FINSEQ_4:def 4; i+1 in dom h0 by A126,A127,FINSEQ_3:27; then A143:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; A144:g1.(h1.i) in rng g1 by A6,A9,A134,BORSUK_1:83,FUNCT_1:def 5; A145:h0.(i+1) in Upper_Arc(P) by A4,A6,A9,A138,A139,BORSUK_1:83,FUNCT_1:def 5; LE h0/.i,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A2,A3,A4,A5,A133,A135,A138,A140,A141,A142,A143,Th19; hence LE h0/.i,h0/.(i+1),P by A4,A133,A142,A143,A144,A145,JORDAN6:def 10; case A146: i>=len h1; now per cases by A146,REAL_1:def 5; case A147:i>len h1; then A148:len h1 +1<=i by NAT_1:38; len h11+1<=i by A21,A147,NAT_1:38; then A149:h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A40,A125,FINSEQ_1:36; A150:i-len h11=i-'len h11 by A21,A147,SCMFSA_7:3; A151: i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A125,REAL_1:49; len h1 +1-len h1<=i-len h1 by A148,REAL_1:49; then 1<=i-'len h11 & i-'len h11<=len mid(h21,2,len h21 -'1) by A21,A150,A151,XCMPLX_1:26; then A152:h0.i=h21.(i-'len h11 +2-'1) by A43,A44,A149,A150,JORDAN3:27; A153:len h1 +1<=i+1 by A148,NAT_1:38; then A154:h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A21,A40,A126,FINSEQ_1:36; i+1>len h11 by A21,A147,NAT_1:38; then A155:i+1-len h11=i+1-'len h11 by SCMFSA_7:3; A156: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A126,REAL_1:49; len h1 +1-len h1<=i+1-len h1 by A153,REAL_1:49; then A157:1<=i+1-'len h11 & i+1-'len h11<=len mid(h21,2,len h21 -'1) by A21,A155,A156,XCMPLX_1:26; then A158:h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A43,A44,A154,A155,JORDAN3:27; 1<i+1-'len h11+(2-1) by A157,NAT_1:38; then 1<i+1-'len h11+2-1 by XCMPLX_1:29; then A159: 0<i+1-'len h11+2-1 by AXIOMS:22; then A160:i+1-'len h11+2-1=i+1-'len h11+2-'1 by BINARITH:def 3; 0<=i-'len h11 by NAT_1:18; then A161: 0+2<=i-'len h11 +2 by AXIOMS:24; i-len h11<=len h1+(len h2-2)-len h11 by A47,A125,REAL_1:49; then i-len h11<=len h2-2 by A21,XCMPLX_1:26; then i-'len h11+2<=len h2-2+2 by A150,AXIOMS:24; then A162: i-'len h11+2<=len h2 by XCMPLX_1:27; then A163:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21 by A23,A161,Lm2,JORDAN3:5,7; set j=i-'len h11+2-'1; A164: j+1=i-'len h11+(1+1)-1+1 by A163,JORDAN3:1 .=i-'len h11+1+1-1+1 by XCMPLX_1:1 .=i-'len h11+1+1 by XCMPLX_1:26 .=i-'len h11+(1+1) by XCMPLX_1:1 .=i-'len h11+2; A165:j+1=i-len h11+2-1+1 by A150,A163,JORDAN3:1 .=1+(i-len h11+(2-1)) by XCMPLX_1:29 .=1+(i+-len h11+(2-1)) by XCMPLX_0:def 8 .=(i+1)+-len h11+(2-1) by XCMPLX_1:1 .=i+1-len h11+(2-1) by XCMPLX_0:def 8 .=i+1-len h11+2-1 by XCMPLX_1:29 .=i+1-'len h11+2-'1 by A155,A159,BINARITH:def 3; A166:j in dom h2 by A22,A163,FINSEQ_3:27; then A167:h0.i=g2.(h2.j) by A152,FUNCT_1:23; A168: h2.j in rng h2 by A166,FUNCT_1:def 5; then A169:0<=h2.j & h2.j<=1 by A16,BORSUK_1:83,TOPREAL5:1; A170:j<j+1 by NAT_1:38; A171:1<j+1 by A163,NAT_1:38; then A172:j+1 in dom h2 by A162,A164,FINSEQ_3:27; then A173:h0.(i+1)=g2.(h2.(j+1)) by A158,A165,FUNCT_1:23; A174: h2.(j+1) in rng h2 by A172,FUNCT_1:def 5; then A175:0<=h2.(j+1) & h2.(j+1)<=1 by A16,BORSUK_1:83,TOPREAL5:1; A176:h2.j<h2.(j+1) by A16,A166,A170,A172,GOBOARD1:def 1; i in dom h0 by A125,FINSEQ_3:27; then A177:h0/.i=h0.i by FINSEQ_4:def 4; i+1 in dom h0 by A126,A127,FINSEQ_3:27; then A178:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; A179:h0.i in Lower_Arc(P) by A13,A15,A16,A167,A168,BORSUK_1:83,FUNCT_1:def 5; A180:h0.(i+1) in Lower_Arc(P) by A13,A15,A16,A173,A174,BORSUK_1:83,FUNCT_1:def 5; i+1-len h11<=len h1+(len h2-2)-len h11 by A47,A126,REAL_1:49; then i+1-'len h11<=len h2-2 by A21,A155,XCMPLX_1:26; then i+1-'len h11+2<=len h2-2+2 by AXIOMS:24; then i+1-'len h11+2<=len h2 by XCMPLX_1:27; then A181:i+1-'len h11+2-1<=len h2-1 by REAL_1:49; len h2<len h2+1 by NAT_1:38; then len h2-1<len h2+1-1 by REAL_1:54; then len h2-1<len h2 by XCMPLX_1:26; then i+1-'len h11+2-'1<len h2 by A160,A181,AXIOMS:22; then A182:i+1-'len h11+2-'1 in dom h2 by A165,A171,FINSEQ_3:27; A183: now assume h0/.(i+1)=W-min(P); then len h21=(i+1-'len h11 +2-'1) by A22,A23,A29,A31,A65,A158,A178,A182,FUNCT_1:def 8; then len h21+1<=len h21-1+1 by A23,A160,A181,AXIOMS:24; then len h21+1<=len h21-(1-1) by XCMPLX_1:37; then len h21+1-len h21<=len h21 -len h21 by REAL_1:49; then len h21+1-len h21<=0 by XCMPLX_1:14; hence contradiction by Lm1,XCMPLX_1:26; end; LE h0/.i,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A11,A12,A13,A14,A167,A169,A173,A175,A176,A177,A178,Th19; hence LE h0/.i,h0/.(i+1),P by A177,A178,A179,A180,A183,JORDAN6:def 10; case A184:i=len h1; then A185:h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A21,A40,A126,FINSEQ_1:36; A186:i+1-len h11=i+1-'len h11 by A21,A128,A184,SCMFSA_7:3; i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A126,REAL_1:49; then A187:i+1-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; 1<=i+1-len h11 by A21,A184,XCMPLX_1:26; then A188:h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A43,A44,A185,A186,A187,JORDAN3:27; A189:h0.i=h11.i by A21,A125,A184,SCMFSA_7:9; i in dom h1 by A125,A184,FINSEQ_3:27; then A190:h0.i=E-max(P) by A5,A9,A184,A189,FUNCT_1:23; i in dom h0 by A125,FINSEQ_3:27; then h0/.i=E-max(P) by A190,FINSEQ_4:def 4; then A191:h0/.i in Upper_Arc(P) by A1,Th1; set j=i-'len h11+2-'1; len h11-'len h11= len h11-len h11 by SCMFSA_7:3.=0 by XCMPLX_1:14; then A192: j=2-1 by A21,A184,SCMFSA_7:3; then A193:j+1<=len h2 by A16,AXIOMS:22; A194:i+1-'len h11+2-'1=1+2-'1 by A21,A184,BINARITH:39 .=2 by BINARITH:39; A195:j+1 in dom h2 by A192,A193,FINSEQ_3:27; then A196:h0.(i+1)=g2.(h2.(j+1)) by A188,A192,A194,FUNCT_1:23; A197: h2.(j+1) in rng h2 by A195,FUNCT_1:def 5; i+1 in dom h0 by A126,A127,FINSEQ_3:27; then A198:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; A199:h0.(i+1) in Lower_Arc(P) by A13,A15,A16,A196,A197,BORSUK_1:83,FUNCT_1:def 5; 2<=len h21 by A16,A23,AXIOMS:22; then A200:2 in dom h21 by FINSEQ_3:27; len h21 <> i+1-'len h11 +2-'1 by A16,A23,A194; then h0/.(i+1) <> W-min P by A22,A23,A29,A31,A65,A188,A194,A198,A200,FUNCT_1:def 8; hence LE h0/.i,h0/.(i+1),P by A191,A198,A199,JORDAN6:def 10; end; hence LE h0/.i,h0/.(i+1),P; end; hence LE h0/.i,h0/.(i+1),P; end; thus for i being Nat,W being Subset of Euclid 2 st 1<=i & i<len h0 & W=Segment(h0/.i,h0/.(i+1),P) holds diameter(W)<e proof let i be Nat,W be Subset of Euclid 2; assume A201:1<=i & i<len h0 & W=Segment(h0/.i,h0/.(i+1),P); then A202:i+1<=len h0 by NAT_1:38; A203:1<i+1 by A201,NAT_1:38; A204:i<i+1 by NAT_1:38; now per cases by REAL_1:def 5; case A205:i<len h1; then A206:i+1<=len h1 by NAT_1:38; A207:h0.i=h11.i by A21,A201,A205,SCMFSA_7:9; A208:i in dom h1 by A201,A205,FINSEQ_3:27; then A209:h11.i=g1.(h1.i) by FUNCT_1:23; then A210:h0.i=g1.(h1.i) by A21,A201,A205,SCMFSA_7:9; A211: h1.i in rng h1 by A208,FUNCT_1:def 5; then A212:0<=h1.i & h1.i<=1 by A9,BORSUK_1:83,TOPREAL5:1; A213:h0.(i+1)=h11.(i+1) by A21,A203,A206,SCMFSA_7:9; A214:i+1 in dom h1 by A203,A206,FINSEQ_3:27; then A215:h0.(i+1)=g1.(h1.(i+1)) by A213,FUNCT_1:23; A216: h1.(i+1) in rng h1 by A214,FUNCT_1:def 5; then A217:0<=h1.(i+1) & h1.(i+1)<=1 by A9,BORSUK_1:83,TOPREAL5:1; A218:h1.i<h1.(i+1) by A9,A204,A208,A214,GOBOARD1:def 1; i in dom h0 by A201,FINSEQ_3:27; then A219:h0/.i=h0.i by FINSEQ_4:def 4; i+1 in dom h0 by A202,A203,FINSEQ_3:27; then A220:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; A221:h0.i in Upper_Arc(P) by A4,A6,A9,A210,A211,BORSUK_1:83,FUNCT_1:def 5; A222:h0.(i+1) in Upper_Arc(P) by A4,A6,A9,A215,A216,BORSUK_1:83,FUNCT_1:def 5; A223:h1/.i=h1.i by A201,A205,FINSEQ_4:24; A224:h1/.(i+1)=h1.(i+1) by A203,A206,FINSEQ_4:24; then reconsider Q1=[.h1/.i,h1/.(i+1).] as Subset of I[01] by A9,A211,A216,A223,BORSUK_1:83,RCOMP_1:16; A225:Segment(h0/.i,h0/.(i+1),P) c= g1.:([.h1/.i,h1/.(i+1).]) proof let x be set;assume A226:x in Segment(h0/.i,h0/.(i+1),P); A227: h0/.(i+1) <> W-min P by A20,A25,A38,A64,A203,A213,A214,A220,FUNCT_1:def 8; then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A226,Def1; then consider p being Point of TOP-REAL 2 such that A228:p=x & (LE h0/.i,p,P & LE p,h0/.(i+1),P); A229:h0/.i in Upper_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) or h0/.i in Upper_Arc(P) & p in Upper_Arc(P) & LE h0/.i,p,Upper_Arc(P),W-min(P),E-max(P) or h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) & LE h0/.i,p,Lower_Arc(P),E-max(P),W-min(P) by A228,JORDAN6:def 10; A230:p in Upper_Arc(P) & h0/.(i+1) in Lower_Arc(P) or p in Upper_Arc(P) & h0/.(i+1) in Upper_Arc(P) & LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) or p in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P)& LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A228,JORDAN6:def 10; now per cases by A206,REAL_1:def 5; case i+1<len h1; then A231: h0/.(i+1) <> E-max P by A20,A26,A37,A64,A213,A214,A220,FUNCT_1:def 8; A232: now assume h0/.(i+1) in Lower_Arc(P); then h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P) by A220,A222,XBOOLE_0:def 3; then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; hence contradiction by A227,A231,TARSKI:def 2; end; then A233:p in Upper_Arc(P) & h0/.(i+1) in Upper_Arc(P) by A228,JORDAN6:def 10; A234: LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A228,A232,JORDAN6:def 10; then A235: p<>E-max(P) by A2,A231,JORDAN6:70; now per cases by A201,REAL_1:def 5; case i>1; then A236: h0/.i <> W-min P by A20,A25,A38,A64,A208,A209,A210,A219,FUNCT_1:def 8; A237: h11.i <> E-max(P) by A20,A26,A37,A64,A205,A208,FUNCT_1:def 8; now assume h0/.i in Lower_Arc(P); then h0/.i in Upper_Arc(P)/\ Lower_Arc(P) by A219,A221,XBOOLE_0:def 3; then h0/.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; hence contradiction by A207,A219,A236,A237,TARSKI:def 2; end; then A238:h0/.i in Upper_Arc(P) & p in Lower_Arc(P) & not p=W-min(P) or h0/.i in Upper_Arc(P) & p in Upper_Arc(P) & LE h0/.i,p,Upper_Arc(P),W-min(P),E-max(P) by A228,JORDAN6:def 10; then A239: p <> W-min P by A2,A236,JORDAN6:69; A240: now assume p in Lower_Arc(P); then p in Upper_Arc(P)/\ Lower_Arc(P) by A233,XBOOLE_0:def 3 ; then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; hence contradiction by A235,A239,TARSKI:def 2; end; then consider z being set such that A241:z in dom g1 & p=g1.z by A4,A238,FUNCT_1:def 5; reconsider rz=z as Real by A6,A241; A242:g1.(h1/.i)=h0/.i by A201,A205,A207,A209,A219,FINSEQ_4:24; A243:0<=h1/.i & h1/.i<=1 & g1.(h1/.(i+1))=h0/.(i+1) by A201,A203,A205,A206,A212,A215,A220,FINSEQ_4:24; h1.(i+1) in rng h1 by A214,FUNCT_1:def 5; then A244:0<=h1/.(i+1) & h1/.(i+1)<=1 by A9,A224,BORSUK_1:83,TOPREAL5:1; take rz; thus rz in dom g1 by A241; A245:0<=rz & rz<=1 by A6,A241,TOPREAL5:1; then A246:h1/.i<=rz by A3,A4,A5,A238,A240,A241,A242,A243,Th20; rz<=h1/.(i+1) by A3,A4,A5,A234,A241,A243,A244,A245,Th20; hence rz in [.h1/.i,h1/.(i+1).] by A246,TOPREAL5:1; thus x = g1.rz by A228,A241; case A247:i=1; now per cases; case A248:p<>W-min(P); now assume p in Lower_Arc(P); then p in Upper_Arc(P)/\ Lower_Arc(P) by A233,XBOOLE_0:def 3; then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; hence contradiction by A235,A248,TARSKI:def 2; end; then consider z being set such that A249:z in dom g1 & p=g1.z by A4,A229,FUNCT_1:def 5; reconsider rz=z as Real by A6,A249; take rz; A250:g1.(h1/.(1+1))=h0/.(1+1) by A206,A215,A220,A247,FINSEQ_4:24; h1.(1+1) in rng h1 by A214,A247,FUNCT_1:def 5; then A251:0<=h1/.(1+1) & h1/.(1+1)<=1 by A9,A224,A247,BORSUK_1:83,TOPREAL5:1; A252:0<=rz & rz<=1 by A6,A249,TOPREAL5:1; A253:h1/.1<=rz by A6,A9,A223,A247,A249,TOPREAL5:1; rz<=h1/.(1+1) by A3,A4,A5,A234,A247,A249,A250,A251,A252,Th20; hence rz in dom g1 & rz in [.h1/.1,h1/.(1+1).] & x = g1.rz by A228,A249,A253,TOPREAL5:1; case A254:p=W-min(P); thus 0 in [.h1/.1,h1/.(1+1).] by A9,A218,A223,A224,A247,TOPREAL5:1; thus x = g1.0 by A5,A228,A254; end; hence ex y being set st y in dom g1 & y in [.h1/.1,h1/.(1+1).] & x = g1.y by A7; end; hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1).] & x = g1.y; case A255:i+1=len h1; then A256:h0/.(i+1)=E-max(P) by A5,A9,A26,A213,A220,FUNCT_1:23; A257:p in Upper_Arc(P) or p in Lower_Arc(P) by A228,JORDAN6:def 10; A258: now assume A259:p in Lower_Arc(P)& not p in Upper_Arc(P); then LE h0/.(i+1),p,Lower_Arc(P),E-max(P),W-min(P) by A11,A256,JORDAN5C:10; hence contradiction by A8,A11,A230,A256,A259,JORDAN5C:12; end; then A260:LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A2,A256,A257,JORDAN5C:10; now per cases; case A261:p<>E-max(P); now per cases; case A262:p<>W-min(P); A263: now assume p in Lower_Arc(P); then p in Upper_Arc(P)/\ Lower_Arc(P) by A258,XBOOLE_0:def 3; then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; hence contradiction by A261,A262,TARSKI:def 2; end; then consider z being set such that A264:z in dom g1 & p=g1.z by A4,A229,FUNCT_1:def 5; reconsider rz=z as Real by A6,A264; take rz; A265: g1.(h1/.(i+1))=h0/.(i+1) by A203,A206,A215,A220,FINSEQ_4:24; h1.(i+1) in rng h1 by A214,FUNCT_1:def 5; then A266:0<=h1/.(i+1) & h1/.(i+1)<=1 by A9,A224,BORSUK_1:83,TOPREAL5:1; A267:0<=rz & rz<=1 by A6,A264,TOPREAL5:1; then A268:h1/.i<=rz by A3,A4,A5,A207,A209,A212,A219,A223,A229,A263,A264,Th20; rz<=h1/.(i+1) by A3,A4,A5,A260,A264,A265,A266,A267,Th20; hence rz in dom g1 & rz in [.h1/.i,h1/.(i+1).] & x = g1.rz by A228,A264,A268,TOPREAL5:1; case A269:p=W-min(P); then h11.i=W-min(P) by A2,A207,A219,A229,JORDAN6:69; then i=1 by A20,A25,A38,A64,A208,FUNCT_1:def 8; then 0 in [.h1/.i,h1/.(i+1).] by A9,A218,A223,A224,TOPREAL5:1; hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1).] & x = g1.y by A5,A7,A228,A269; end; hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1).] & x = g1.y; case A270:p=E-max(P); 1 in [.h1/.i,h1/.(i+1).] by A9,A218,A223,A224,A255,TOPREAL5:1; hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1).] & x = g1.y by A5,A33,A228,A270,Lm6; end; hence ex y being set st y in dom g1 & y in [.h1/.i, h1/.(i+1).] & x = g1.y; end; hence x in g1.:([.h1/.i,h1/.(i+1).]) by FUNCT_1:def 12; end; g1.:([.h1/.i,h1/.(i+1).]) c= Segment(h0/.i,h0/.(i+1),P) proof let x be set;assume x in g1.:([.h1/.i,h1/.(i+1).]); then consider y being set such that A271: y in dom g1 & y in [.h1/.i,h1/.(i+1).] & x=g1.y by FUNCT_1:def 12; A272:x in Upper_Arc(P) by A4,A271,FUNCT_1:def 5; then reconsider p1=x as Point of TOP-REAL 2; reconsider sy=y as Real by A271; A273:g1.(h1/.i)=h0/.i by A201,A205,A210,A219,FINSEQ_4:24; A274:h1/.i<=sy & sy<=h1/.(i+1) by A271,TOPREAL5:1; A275:0<=h1/.i & h1/.i<=1 by A201,A205,A212,FINSEQ_4:24; A276:0<=sy & sy<=1 by A6,A271,TOPREAL5:1; then A277: LE h0/.i,p1,Upper_Arc(P),W-min(P),E-max(P) by A2,A3,A4,A5,A271,A273,A274,A275,Th19; LE p1,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A2,A3,A4,A5,A215,A217,A220,A224,A271,A274,A276,Th19; then A278: LE h0/.i,p1,P & LE p1,h0/.(i+1),P by A219,A220,A221,A222,A272,A277,JORDAN6:def 10; A279: not h0/.(i+1)=W-min P by A20,A25,A38,A64,A203,A213,A214,A220,FUNCT_1:def 8; x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A278; hence x in Segment(h0/.i,h0/.(i+1),P) by A279,Def1; end; then W=g1.:Q1 by A201,A225,XBOOLE_0:def 10; hence diameter(W)<e by A9,A201,A205; case A280:i>len h1; then A281:len h1 +1<=i by NAT_1:38; len h11+1<=i & i<=len h11 + len (mid(h21,2,len h21 -'1)) by A21,A201,A280,FINSEQ_1:35,NAT_1:38; then A282:h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by FINSEQ_1:36; A283:i-len h11=i-'len h11 by A21,A280,SCMFSA_7:3; A284: i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A201,REAL_1:49; len h1 +1-len h1<=i-len h1 by A281,REAL_1:49; then 1<=i-'len h11 & i-'len h11<=len mid(h21,2,len h21 -'1) by A21,A283,A284,XCMPLX_1:26; then A285:h0.i=h21.(i-'len h11 +2-'1) by A43,A44,A282,A283,JORDAN3:27; A286:len h1 +1<=i+1 by A281,NAT_1:38; then A287:h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A21,A40,A202,FINSEQ_1:36; i+1>len h11 by A21,A280,NAT_1:38; then A288:i+1-len h11=i+1-'len h11 by SCMFSA_7:3; A289: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A202,REAL_1:49; len h1 +1-len h1<=i+1-len h1 by A286,REAL_1:49; then A290:1<=i+1-'len h11 & i+1-'len h11<=len mid(h21,2,len h21 -'1) by A21,A288,A289,XCMPLX_1:26; then A291:h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A43,A44,A287,A288,JORDAN3:27; 1<i+1-'len h11+(2-1) by A290,NAT_1:38; then 1<i+1-'len h11+2-1 by XCMPLX_1:29; then 0<i+1-'len h11+2-1 by AXIOMS:22; then A292:i+1-'len h11+2-1=i+1-'len h11+2-'1 by BINARITH:def 3; 0<=i-'len h11 by NAT_1:18; then A293: 0+2<=i-'len h11 +2 by AXIOMS:24; i-len h11<=len h1+(len h2-2)-len h11 by A47,A201,REAL_1:49; then i-len h11<=(len h2-2) by A21,XCMPLX_1:26; then i-'len h11+2<=len h2-2+2 by A283,AXIOMS:24; then A294: i-'len h11+2<=len h2 by XCMPLX_1:27; then A295:i-'len h11+2-1<=len h2-1 by REAL_1:49; A296:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21 by A23,A293,A294,Lm2,JORDAN3:5,7; len h2<len h2+1 by NAT_1:38; then len h2-1<len h2+1-1 by REAL_1:54; then len h2-1<len h2 by XCMPLX_1:26; then A297:i-'len h11+2-1<len h2 by A295,AXIOMS:22; A298:i-'len h11+2-'1=i-'len h11+2-1 by A296,JORDAN3:1; set j=i-'len h11+2-'1; len h1 +1<=i by A280,NAT_1:38; then len h11+1-len h11<=i-len h11 by A21,REAL_1:49; then 1<=i-len h11 by XCMPLX_1:26; then 1<=i-'len h11 by JORDAN3:1; then 1+2<=i-'len h11+2 by AXIOMS:24; then 1+2-1<=i-'len h11+2-1 by REAL_1:49; then A299:1<j by A298,AXIOMS:22; i-len h11<len h11+(len h2-2)-len h11 by A21,A47,A201,REAL_1:54; then i-len h11<len h2-2 by XCMPLX_1:26; then A300: i-len h11+2<len h2-2+2 by REAL_1:53; A301:j< len h2 by A296,A297,JORDAN3:1; A302:j+1=i-'len h11+(1+1)-1+1 by A296,JORDAN3:1 .=i-'len h11+1+1-1+1 by XCMPLX_1:1 .=i-'len h11+1+1 by XCMPLX_1:26 .=i-'len h11+(1+1) by XCMPLX_1:1; then A303:j+1<len h2 by A283,A300,XCMPLX_1:27; A304:j+1 =1+(i-len h11+(2-1)) by A283,A298,XCMPLX_1:29 .=1+(i+-len h11+(2-1)) by XCMPLX_0:def 8 .=(i+1)+-len h11+(2-1) by XCMPLX_1:1 .=i+1-len h11+(2-1) by XCMPLX_0:def 8 .=i+1-'len h11+2-'1 by A288,A292,XCMPLX_1:29; A305:j in dom h2 by A22,A296,FINSEQ_3:27; then A306:h0.i=g2.(h2.j) by A285,FUNCT_1:23; A307: h2.j in rng h2 by A305,FUNCT_1:def 5; A308:1<j+1 by A296,NAT_1:38; then A309:j+1 in dom h2 by A294,A302,FINSEQ_3:27; then A310: h0.(i+1)=g2.(h2.(j+1)) by A291,A304,FUNCT_1:23; A311: h2.(j+1) in rng h2 by A309,FUNCT_1:def 5; i in dom h0 by A201,FINSEQ_3:27; then A312:h0/.i=h0.i by FINSEQ_4:def 4; i+1 in dom h0 by A202,A203,FINSEQ_3:27; then A313:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; g2.(h2.j) in rng g2 by A15,A16,A307,BORSUK_1:83,FUNCT_1:def 5; then A314:h0.i in Lower_Arc(P) by A13,A285,A305,FUNCT_1:23; A315:h0.(i+1) in Lower_Arc(P) by A13,A15,A16,A310,A311,BORSUK_1:83,FUNCT_1:def 5; A316: 0 <= h2.j by A16,A307,BORSUK_1:83,TOPREAL5:1; A317: h2.j <= 1 by A16,A307,BORSUK_1:83,TOPREAL5:1; A318: g2.(h2.(j+1)) = h0/.(i+1) by A291,A304,A309,A313,FUNCT_1:23; A319: h2.(j+1) <= 1 by A16,A311,BORSUK_1:83,TOPREAL5:1; A320:h2/.j=h2.j by A296,A301,FINSEQ_4:24; A321:h2/.(j+1)=h2.(j+1) by A294,A302,A308,FINSEQ_4:24; then reconsider Q1=[.h2/.j,h2/.(j+1).] as Subset of I[01] by A16,A307,A311,A320,BORSUK_1:83,RCOMP_1:16; A322:Segment(h0/.i,h0/.(i+1),P) c= g2.:([.h2/.j,h2/.(j+1).]) proof let x be set;assume A323:x in Segment(h0/.i,h0/.(i+1),P); h0/.(i+1) <> W-min P by A22,A29,A31,A65,A291,A303,A304,A309,A313,FUNCT_1:def 8; then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A323,Def1; then consider p being Point of TOP-REAL 2 such that A324:p=x & (LE h0/.i,p,P & LE p,h0/.(i+1),P); A325:h0/.i in Upper_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) or h0/.i in Upper_Arc(P) & p in Upper_Arc(P) & LE h0/.i,p,Upper_Arc(P),W-min(P),E-max(P) or h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) & LE h0/.i,p,Lower_Arc(P),E-max(P),W-min(P) by A324,JORDAN6:def 10; A326:j<len h2 by A294,A302,NAT_1:38; A327: h0/.(i+1) <> E-max P by A22,A28,A30,A65,A291,A304,A308,A309,A313,FUNCT_1:def 8; A328: h21.(j+1) <> W-min P by A22,A29,A31,A65,A303,A309,FUNCT_1:def 8; now assume h0/.(i+1) in Upper_Arc(P); then h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P) by A313,A315,XBOOLE_0:def 3; then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; hence contradiction by A291,A304,A313,A327,A328,TARSKI:def 2; end; then A329:p in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P)& not h0/.(i+1)=W-min(P) & LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) or p in Upper_Arc(P) & h0/.(i+1) in Lower_Arc(P) & not h0/.(i+1)=W-min(P) by A324,JORDAN6:def 10; A330: h0/.i <> W-min(P) by A22,A29,A31,A65,A285,A305,A312,A326,FUNCT_1:def 8; A331: h21.j <> E-max P by A22,A28,A30,A65,A299,A305,FUNCT_1:def 8; A332: now assume h0/.i in Upper_Arc(P); then h0/.i in Upper_Arc(P)/\ Lower_Arc(P) by A312,A314,XBOOLE_0:def 3; then h0/.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; hence contradiction by A285,A312,A330,A331,TARSKI:def 2; end; then A333: LE h0/.i,p,Lower_Arc P, E-max P, W-min P by A324,JORDAN6:def 10; A334: h0/.i <> E-max(P) by A22,A28,A30,A65,A285,A299,A305,A312,FUNCT_1: def 8; A335: now assume p in Upper_Arc(P); then p in Upper_Arc P /\ Lower_Arc P by A325,A332,XBOOLE_0: def 3; then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; then p=W-min(P) or p=E-max(P) by TARSKI:def 2; hence contradiction by A11,A325,A332,A334,JORDAN6:69; end; then A336: LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A324,JORDAN6:def 10; consider z being set such that A337:z in dom g2 & p=g2.z by A13,A329,A335,FUNCT_1:def 5; reconsider rz=z as Real by A15,A337; A338:g2.(h2/.(j+1))=h0/.(i+1) by A291,A304,A309,A313,A321,FUNCT_1:23; A339:0<=h2/.j & h2/.j<=1 by A16,A307,A320,BORSUK_1:83,TOPREAL5:1; h2.(j+1) in rng h2 by A309,FUNCT_1:def 5; then 0<=rz & rz<=1 & 0<=h2/.(j+1) & h2/.(j+1)<=1 by A15,A16,A321,A337,BORSUK_1:83,TOPREAL5:1; then rz<=h2/.(j+1)& h2/.j<=rz by A12,A13,A14,A306,A312,A320,A333,A336,A337,A338,A339,Th20; then rz in [.h2/.j,h2/.(j+1).] by TOPREAL5:1; hence x in g2.:([.h2/.j,h2/.(j+1).]) by A324,A337,FUNCT_1:def 12; end; g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.(i+1),P) proof let x be set;assume x in g2.:([.h2/.j,h2/.(j+1).]); then consider y being set such that A340: y in dom g2 & y in [.h2/.j,h2/.(j+1).] & x=g2.y by FUNCT_1:def 12; A341:x in Lower_Arc(P) by A13,A340,FUNCT_1:def 5; then reconsider p1=x as Point of TOP-REAL 2; reconsider sy=y as Real by A340; A342:h2/.j<=sy & sy<=h2/.(j+1) by A340,TOPREAL5:1; A343:0<=sy & sy<=1 by A15,A340,TOPREAL5:1; A344: h2.(j+1) <> 1 by A16,A18,A29,A303,A309,FUNCT_1:def 8; A345: now assume p1=W-min(P); then 1=sy by A12,A14,A32,A340,FUNCT_1:def 8; hence contradiction by A319,A321,A342,A344,AXIOMS:21; end; A346: h0/.(i+1) <> W-min P by A22,A29,A31,A65,A291,A303,A304,A309,A313,FUNCT_1:def 8; A347: LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P) by A11,A12,A13,A14,A306,A312,A316,A317,A320,A340,A342,A343, Th19; LE p1,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A11,A12,A13,A14,A318,A319,A321,A340,A342,A343,Th19; then LE h0/.i,p1,P & LE p1,h0/.(i+1),P by A312,A313,A314,A315,A341,A345,A346,A347,JORDAN6:def 10; then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P}; hence x in Segment(h0/.i,h0/.(i+1),P) by A346,Def1; end; then W=g2.:(Q1) by A201,A322,XBOOLE_0:def 10; hence diameter(W)<e by A16,A296,A301; case A348:i=len h1; then A349:h0.i=E-max(P) by A21,A37,A201,SCMFSA_7:9; A350:i-len h11=i-'len h11 by A21,A348,SCMFSA_7:3; A351:h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A21,A40,A202,A348,FINSEQ_1:36; A352:i+1-len h11=i+1-'len h11 by A21,A204,A348,SCMFSA_7:3; i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A202,REAL_1:49; then A353:1<=i+1-'len h11 & i+1-'len h11<=len mid(h21,2,len h21 -'1) by A21,A348,A352,XCMPLX_1:26; then 1<i+1-'len h11+(2-1) by NAT_1:38; then 1<i+1-'len h11+2-1 by XCMPLX_1:29; then 0<i+1-'len h11+2-1 by AXIOMS:22; then A354:i+1-'len h11+2-1=i+1-'len h11+2-'1 by BINARITH:def 3; 0<=i-'len h11 by NAT_1:18; then A355: 0+2<=i-'len h11 +2 by AXIOMS:24; i-len h11<=len h1+(len h2-2)-len h11 by A47,A201,REAL_1:49; then i-len h11<=(len h2-2) by A21,XCMPLX_1:26; then i-'len h11+2<=len h2-2+2 by A350,AXIOMS:24; then A356: i-'len h11+2<=len h2 by XCMPLX_1:27; then A357:i-'len h11+2-1<=len h2-1 by REAL_1:49; A358:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21 by A23,A355,A356,Lm2,JORDAN3:5,7; len h2<len h2+1 by NAT_1:38; then len h2-1<len h2+1-1 by REAL_1:54; then len h2-1<len h2 by XCMPLX_1:26; then A359:i-'len h11+2-1<len h2 by A357,AXIOMS:22; A360:i-'len h11+2-'1=i-'len h11+2-1 by A358,JORDAN3:1; set j=i-'len h11+2-'1; len h1-len h11>=0 by A21,XCMPLX_1:14; then len h1-'len h11=len h11-len h11 by A21,BINARITH:def 3; then A361: 0+2-1=len h1-'len h11+2-1 by XCMPLX_1:14; A362:0<=i-len h11 by A21,A348,XCMPLX_1:14; i-len h11<len h11+(len h2-2)-len h11 by A21,A47,A201,REAL_1:54; then i-len h11<len h2-2 by XCMPLX_1:26; then i-len h11+2<len h2-2+2 by REAL_1:53; then A363:i-len h11+2<len h2 by XCMPLX_1:27; A364:j+1=i-'len h11+(1+1)-1+1 by A358,JORDAN3:1 .=i-'len h11+1+1-1+1 by XCMPLX_1:1 .=i-'len h11+1+1 by XCMPLX_1:26 .=i-'len h11+(1+1) by XCMPLX_1:1; then A365:j+1<len h2 by A362,A363,BINARITH:def 3; A366:j+1=i-len h11+2-1+1 by A360,A362,BINARITH:def 3 .=1+(i-len h11+(2-1)) by XCMPLX_1:29 .=1+(i+-len h11+(2-1)) by XCMPLX_0:def 8 .=(i+1)+-len h11+(2-1) by XCMPLX_1:1 .=i+1-len h11+(2-1) by XCMPLX_0:def 8 .=i+1-'len h11+2-'1 by A352,A354,XCMPLX_1:29; A367:j in dom h2 by A22,A358,FINSEQ_3:27; then A368:h21.j=g2.(h2.j) by FUNCT_1:23; A369:h0.i=g2.(h2.j) by A14,A16,A348,A349,A361,JORDAN3:1; A370: h2.j in rng h2 by A367,FUNCT_1:def 5; A371:1<j+1 by A358,NAT_1:38; A372: h0.(i+1)=h21.(j+1) by A43,A44,A351,A352,A353,A366,JORDAN3:27; A373:j+1 in dom h2 by A356,A364,A371,FINSEQ_3:27; then A374:h0.(i+1)=g2.(h2.(j+1)) by A372,FUNCT_1:23; A375: h2.(j+1) in rng h2 by A373,FUNCT_1:def 5; i in dom h0 by A201,FINSEQ_3:27; then A376:h0/.i=h0.i by FINSEQ_4:def 4; i+1 in dom h0 by A202,A203,FINSEQ_3:27; then A377:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; g2.(h2.j) in rng g2 by A15,A16,A370,BORSUK_1:83,FUNCT_1:def 5; then A378:h0.i in Lower_Arc P by A13,A14,A16,A348,A349,A361,JORDAN3:1; A379:h0.(i+1) in Lower_Arc P by A13,A15,A16,A374,A375,BORSUK_1:83,FUNCT_1:def 5; A380:1<=j & j<len h2 by A358,A359,JORDAN3:1; A381: g2.(h2.(j+1)) = h0/.(i+1) by A372,A373,A377,FUNCT_1:23; A382: h2.(j+1) <= 1 by A16,A375,BORSUK_1:83,TOPREAL5:1; A383:h2/.j=h2.j by A380,FINSEQ_4:24; A384:h2/.(j+1)=h2.(j+1) by A356,A364,A371,FINSEQ_4:24; then reconsider Q1=[.h2/.j,h2/.(j+1).] as Subset of I[01] by A16,A370,A375,A383,BORSUK_1:83,RCOMP_1:16; A385:Segment(h0/.i,h0/.(i+1),P) c= g2.:([.h2/.j,h2/.(j+1).]) proof let x be set;assume A386:x in Segment(h0/.i,h0/.(i+1),P); h0/.(i+1) <> W-min P by A22,A29,A31,A65,A365,A372,A373,A377,FUNCT_1:def 8; then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A386,Def1; then consider p being Point of TOP-REAL 2 such that A387:p=x & LE h0/.i,p,P & LE p,h0/.(i+1),P; A388:h0/.i in Upper_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) or h0/.i in Upper_Arc(P) & p in Upper_Arc(P) & LE h0/.i,p,Upper_Arc(P),W-min(P),E-max(P) or h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) & LE h0/.i,p,Lower_Arc(P),E-max(P),W-min(P) by A387,JORDAN6:def 10; j+1<len h2 by A362,A363,A364,BINARITH:def 3; then A389:j<len h2 by NAT_1:38; A390:not h0/.(i+1)=E-max(P) by A22,A28,A30,A65,A371,A372,A373,A377,FUNCT_1:def 8; A391:h0/.(i+1) in Lower_Arc(P) by A13,A15,A16,A374,A375,A377,BORSUK_1:83,FUNCT_1:def 5; now assume h0/.(i+1) in Upper_Arc(P); then h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P) by A391,XBOOLE_0:def 3; then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; then h21.(j+1)=W-min(P) by A372,A377,A390,TARSKI:def 2; hence contradiction by A22,A29,A31,A65,A365,A373,FUNCT_1:def 8; end; then A392:p in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P) & not h0/.(i+1)=W-min(P) & LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) or p in Upper_Arc(P) & h0/.(i+1) in Lower_Arc(P) & not h0/.(i+1)=W-min(P) by A387,JORDAN6:def 10; A393:h0/.i<>W-min(P) by A22,A29,A31,A65,A367,A368,A369,A376,A389,FUNCT_1:def 8; dom (g1*h1) c= dom h0 by FINSEQ_1:39; then A394: h0/.i=E-max(P) by A36,A348,A349,FINSEQ_4:def 4; A395: now assume A396:not p in Lower_Arc(P); then p=E-max(P) by A2,A388,A394,JORDAN6:70; hence contradiction by A1,A396,Th1; end; A397: now assume p in Upper_Arc(P); then p in Upper_Arc(P)/\ Lower_Arc(P) by A395,XBOOLE_0:def 3 ; then A398: p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; p <> W-min P by A2,A388,A393,JORDAN6:69; hence p = E-max P by A398,TARSKI:def 2; end; then A399: LE p,h0/.(i+1),Lower_Arc P, E-max P, W-min P by A11,A392,JORDAN5C:10; p in rng g2 by A1,A13,A387,A397,Th1,JORDAN6:def 10; then consider z being set such that A400:z in dom g2 & p=g2.z by FUNCT_1:def 5; reconsider rz=z as Real by A15,A400; A401: g2.(h2/.(j+1))=h0/.(i+1) by A356,A364,A371,A374,A377,FINSEQ_4:24; h2.(j+1) in rng h2 by A373,FUNCT_1:def 5; then 0<=rz & rz<=1 & 0<=h2/.(j+1) & h2/.(j+1)<=1 by A15,A16,A384,A400,BORSUK_1:83,TOPREAL5:1; then rz<=h2/.(j+1)& h2/.j<=rz by A12,A13,A14,A16,A348,A361,A383,A399,A400,A401,Th20,JORDAN3: 1; then rz in [.h2/.j,h2/.(j+1).] by TOPREAL5:1; hence x in g2.:([.h2/.j,h2/.(j+1).]) by A387,A400,FUNCT_1:def 12; end; g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.(i+1),P) proof let x be set;assume x in g2.:([.h2/.j,h2/.(j+1).]); then consider y being set such that A402: y in dom g2 & y in [.h2/.j,h2/.(j+1).] & x=g2.y by FUNCT_1:def 12; A403:x in Lower_Arc(P) by A13,A402,FUNCT_1:def 5; then reconsider p1=x as Point of TOP-REAL 2; reconsider sy=y as Real by A402; A404:h2/.j<=sy & sy<=h2/.(j+1) by A402,TOPREAL5:1; A405:0<=sy & sy<=1 by A15,A402,TOPREAL5:1; A406: h2.(j+1) <> 1 by A16,A18,A29,A365,A373,FUNCT_1:def 8; A407: now assume p1=W-min(P); then 1=sy by A12,A14,A32,A402,FUNCT_1:def 8; hence contradiction by A382,A384,A404,A406,AXIOMS:21; end; A408: h0/.(i+1) <> W-min(P) by A22,A29,A31,A65,A365,A372,A373,A377,FUNCT_1:def 8; LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P) by A11,A12,A13,A14,A349,A376,A402,A405,Th19; then A409: LE h0/.i,p1,P by A376,A378,A403,A407,JORDAN6:def 10; LE p1,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A11,A12,A13,A14,A381,A382,A384,A402,A404,A405,Th19; then LE p1,h0/.(i+1),P by A377,A379,A403,A408,JORDAN6:def 10; then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A409; hence x in Segment(h0/.i,h0/.(i+1),P) by A408,Def1; end; then W=g2.:(Q1) by A201,A385,XBOOLE_0:def 10; hence diameter(W)<e by A16,A380; end; hence diameter(W)<e; end; thus for W being Subset of Euclid 2 st W=Segment(h0/.len h0,h0/.1,P) holds diameter W < e proof let W be Subset of Euclid 2; assume A410: W=Segment(h0/.len h0,h0/.1,P); set i=len h0; len h0<=len h11 + len mid(h21,2,len h21 -'1) by FINSEQ_1:35; then A411: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A21,A48, FINSEQ_1:36; A412:i-len h11=i-'len h11 by A21,A49,SCMFSA_7:3; i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by FINSEQ_1:35; then A413:i-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; len h1 +1-len h1<=i-len h1 by A48,REAL_1:49; then 1<=i-len h1 by XCMPLX_1:26; then A414:h0.i=h21.(i-'len h11 +2-'1) by A21,A43,A44,A411,A412,A413,JORDAN3:27; A415:i-'len h11+2 =(len h21-2)+2 by A21,A23,A47,A412,XCMPLX_1:26 .=len h21 by XCMPLX_1:27; 0<=i-'len h11 by NAT_1:18; then A416: 0+2<=i-'len h11 +2 by AXIOMS:24; then A417: 2-'1<=(i-'len h11 +2-'1) by JORDAN3:5; i-'len h11+2<=len h2-2+2 by A21,A47,A412,XCMPLX_1:26; then A418: i-'len h11+2<=len h2 by XCMPLX_1:27; then A419:i-'len h11+2-1<=len h2-1 by REAL_1:49; A420:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21 by A23,A416,A418,Lm2,JORDAN3:5,7; len h2<len h2+1 by NAT_1:38; then len h2-1<len h2+1-1 by REAL_1:54; then len h2-1<len h2 by XCMPLX_1:26; then A421:i-'len h11+2-1<len h2 by A419,AXIOMS:22; A422:i-'len h11+2-'1=i-'len h11+2-1 by A417,Lm2,JORDAN3:1; set j=i-'len h11+2-'1; len h11+1-len h11<=i-len h11 by A21,A48,REAL_1:49; then 1<=i-len h11 by XCMPLX_1:26; then 1<=i-'len h11 by JORDAN3:1; then 1+2<=i-'len h11+2 by AXIOMS:24; then 1+2-1<=i-'len h11+2-1 by REAL_1:49; then A423:1<j by A422,AXIOMS:22; A424:j< len h2 by A417,A421,Lm2,JORDAN3:1; A425:j+1=i-'len h11+(1+1)-1+1 by A417,Lm2,JORDAN3:1 .=i-'len h11+1+1-1+1 by XCMPLX_1:1 .=i-'len h11+1+1 by XCMPLX_1:26 .=i-'len h11+(1+1) by XCMPLX_1:1; A426:j in dom h2 by A22,A420,FINSEQ_3:27; then A427:h0.i=g2.(h2.j) by A414,FUNCT_1:23; A428: h2.j in rng h2 by A426,FUNCT_1:def 5; then A429:0<=h2.j & h2.j<=1 by A16,BORSUK_1:83,TOPREAL5:1; A430:1<j+1 by A417,Lm2,NAT_1:38; A431:h0.i in Lower_Arc P by A13,A15,A16,A427,A428,BORSUK_1:83,FUNCT_1:def 5; A432: now assume h0.i in Upper_Arc(P); then h0.i in Upper_Arc(P)/\ Lower_Arc(P) by A431,XBOOLE_0:def 3; then h0.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; then h0.i=W-min(P) or h0.i=E-max(P) by TARSKI:def 2; hence contradiction by A22,A28,A29,A30,A31,A65,A414,A423,A424,A426,FUNCT_1:def 8; end; j+1 in dom h2 by A22,A415,A425,A430,FINSEQ_3:27; then A433: h2.(j+1) in rng h2 by FUNCT_1:def 5; i in dom h0 by A50,FINSEQ_3:27; then A434:h0/.i=h0.i by FINSEQ_4:def 4; A435: 0 <= h2.j by A16,A428,BORSUK_1:83,TOPREAL5:1; A436: h2.j <= 1 by A16,A428,BORSUK_1:83,TOPREAL5:1; A437:h2/.j=h2.j by A417,A424,Lm2,FINSEQ_4:24; A438:h2/.(j+1)=h2.(j+1) by A418,A425,A430,FINSEQ_4:24; then reconsider Q1=[.h2/.j,h2/.(j+1).] as Subset of I[01] by A16,A428,A433,A437,BORSUK_1:83,RCOMP_1:16; A439:Segment(h0/.i,h0/.1,P) c= g2.:([.h2/.j,h2/.(j+1).]) proof let x be set;assume A440:x in Segment(h0/.i,h0/.1,P); h0/.1=W-min(P) by A39,A61,FINSEQ_4:def 4; then x in {p: LE h0/.i,p,P or h0/.i in P & p=W-min(P)} by A440,Def1; then consider p being Point of TOP-REAL 2 such that A441:p=x & (LE h0/.i,p,P or h0/.i in P & p=W-min(P)); A442:j<j+1 by NAT_1:38; A443:j in dom h2 by A417,A424,Lm2,FINSEQ_3:27; j+1 in dom h2 by A418,A425,A430,FINSEQ_3:27; then h2.j<h2.(j+1) by A16,A442,A443,GOBOARD1:def 1; then A444:h2/.(j+1) in [.h2/.j, h2/.(j+1).] by A437,A438,RCOMP_1:15; A445: h2/.(j+1)=1 by A16,A23,A29,A415,A425,FINSEQ_4:def 4; now per cases by A441; case LE h0/.i,p,P & (p<>W-min(P) or not h0/.i in P); then A446:h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) & LE h0/.i,p,Lower_Arc(P),E-max(P),W-min(P) by A432,A434,JORDAN6:def 10; then consider z being set such that A447:z in dom g2 & p=g2.z by A13,FUNCT_1:def 5; reconsider rz=z as Real by A15,A447; take rz; A448: 0<=rz & rz<=1 by A15,A447,TOPREAL5:1; then A449: h2/.j<=rz by A12,A13,A14,A427,A429,A434,A437,A446,A447,Th20; thus rz in dom g2 by A447; rz<=h2/.(j+1) by A16,A22,A415,A425,A438,A448,FINSEQ_3:31; hence rz in [.h2/.j,h2/.(j+1).] & x = g2.rz by A441,A447,A449,TOPREAL5:1; case h0/.i in P & p=W-min(P); hence ex y being set st y in dom g2 & y in [.h2/.j,h2/.(j+1).] & x = g2.y by A14,A32,A441,A444,A445; end; hence x in g2.:([.h2/.j,h2/.(j+1).]) by FUNCT_1:def 12; end; g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.1,P) proof let x be set;assume x in g2.:([.h2/.j,h2/.(j+1).]); then consider y being set such that A450: y in dom g2 & y in [.h2/.j,h2/.(j+1).] & x=g2.y by FUNCT_1:def 12; A451:x in Lower_Arc(P) by A13,A450,FUNCT_1:def 5; then reconsider p1=x as Point of TOP-REAL 2; reconsider sy=y as Real by A450; A452:h2/.j<=sy & sy<=h2/.(j+1) by A450,TOPREAL5:1; A453:0<=sy & sy<=1 by A15,A450,TOPREAL5:1; A454:h0/.1=W-min(P) by A39,A61,FINSEQ_4:def 4; A455: Upper_Arc(P) \/ Lower_Arc(P)=P by A1,JORDAN6:def 9; A456: LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P) by A11,A12,A13,A14,A427,A434,A435,A436,A437,A450,A452,A453,Th19; now per cases; case p1=W-min(P); hence LE h0/.i,p1,P or h0/.i in P & p1=W-min(P) by A431,A434,A455,XBOOLE_0:def 2; case p1<>W-min(P); hence LE h0/.i,p1,P or h0/.i in P & p1=W-min(P) by A431,A434,A451,A456,JORDAN6:def 10; end; then x in {p: LE h0/.i,p,P or h0/.i in P & p=W-min(P)}; hence x in Segment(h0/.i,h0/.1,P) by A454,Def1; end; then W=g2.:Q1 by A410,A439,XBOOLE_0:def 10; hence diameter(W)<e by A16,A417,A424,Lm2; end; A457: for i being Nat st 1<=i & i+1<len h0 holds LE h0/.(i+1),h0/.(i+2),P proof let i be Nat;assume A458: 1<=i & i+1<len h0; then A459:i+1+1<=len h0 by NAT_1:38; A460:1<i+1 by A458,NAT_1:38; then A461:1<i+1+1 by NAT_1:38; A462: i+1<i+1+1 by NAT_1:38; now per cases; case A463:i+1<len h1; then A464:i+1+1<=len h1 by NAT_1:38; A465:h0.(i+1)=h11.(i+1) by A21,A460,A463,SCMFSA_7:9; A466:i+1 in dom h1 by A460,A463,FINSEQ_3:27; then A467:h0.(i+1)=g1.(h1.(i+1)) by A465,FUNCT_1:23; A468: h1.(i+1) in rng h1 by A466,FUNCT_1:def 5; then A469:0<=h1.(i+1) & h1.(i+1)<=1 by A9,BORSUK_1:83,TOPREAL5:1; A470:1<i+1+1 by A460,NAT_1:38; then A471:h0.(i+1+1)=h11.(i+1+1) by A21,A464,SCMFSA_7:9; A472:i+1+1 in dom h1 by A464,A470,FINSEQ_3:27; then A473:h0.(i+1+1)=g1.(h1.(i+1+1)) by A471,FUNCT_1:23; A474: h1.((i+1)+1) in rng h1 by A472,FUNCT_1:def 5; then A475: 0<=h1.(i+1+1) by A9,BORSUK_1:83,TOPREAL5:1; A476: h1.(i+1+1)<=1 by A9,A474,BORSUK_1:83,TOPREAL5:1; A477:h1.(i+1)<h1.(i+1+1) by A9,A462,A466,A472,GOBOARD1:def 1; i+1 in dom h0 by A458,A460,FINSEQ_3:27; then A478:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; (i+1)+1 in dom h0 by A459,A470,FINSEQ_3:27; then A479:h0/.(i+1+1)=h0.(i+1+1) by FINSEQ_4:def 4; A480:g1.(h1.(i+1)) in rng g1 by A6,A9,A468,BORSUK_1:83,FUNCT_1:def 5; A481: i+1+1=i+(1+1) by XCMPLX_1:1; A482: h0/.(i+1) in Upper_Arc P by A4,A465,A466,A478,A480,FUNCT_1:23; A483: h0/.(i+1+1) in Upper_Arc P by A4,A6,A9,A473,A474,A479,BORSUK_1:83,FUNCT_1:def 5; LE h0/.(i+1),h0/.((i+1)+1),Upper_Arc(P),W-min(P),E-max(P) by A2,A3,A4,A5,A467,A469,A473,A475,A476,A477,A478,A479,Th19; hence thesis by A481,A482,A483,JORDAN6:def 10; case A484: i+1>=len h1; now per cases by A484,REAL_1:def 5; case A485:i+1>len h1; then A486:len h1 +1<=i+1 by NAT_1:38; A487: len h11+1<=i+1 by A21,A485,NAT_1:38; A488: i+1<=len h11 + len (mid(h21,2,len h21 -'1)) by A458,FINSEQ_1:35; then A489:h0.(i+1)=(mid(h21,2,len h21 -'1)).((i+1) -len h11) by A487,FINSEQ_1:36; A490:(i+1)-len h11=(i+1)-'len h11 by A21,A485,SCMFSA_7:3; (i+1)-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A488,REAL_1:49; then A491:(i+1)-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; len h1 +1-len h1<=(i+1)-len h1 by A486,REAL_1:49; then 1<=(i+1)-'len h11 by A21,A490,XCMPLX_1:26; then A492:h0.(i+1)=h21.((i+1)-'len h11 +2-'1) by A43,A44,A489,A490,A491,JORDAN3:27; A493:len h1 +1<=(i+1)+1 by A486,NAT_1:38; then A494:h0.((i+1)+1)=(mid(h21,2,len h21 -'1)).((i+1)+1 -len h11) by A21,A40,A459,FINSEQ_1:36; (i+1)+1>len h11 by A21,A485,NAT_1:38; then A495:(i+1)+1-len h11=(i+1)+1-'len h11 by SCMFSA_7:3; A496: (i+1)+1-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A459,REAL_1:49; len h1 +1-len h1<=(i+1)+1-len h1 by A493,REAL_1:49; then A497:1<=(i+1)+1-'len h11 & (i+1)+1-'len h11<=len mid(h21,2,len h21 -'1) by A21,A495,A496,XCMPLX_1:26; then A498:h0.((i+1)+1)=h21.((i+1)+1-'len h11 +2-'1) by A43,A44,A494,A495,JORDAN3:27; 1<(i+1)+1-'len h11+(2-1) by A497,NAT_1:38; then 1<(i+1)+1-'len h11+2-1 by XCMPLX_1:29; then A499: 0<(i+1)+1-'len h11+2-1 by AXIOMS:22; 0<=(i+1)-'len h11 by NAT_1:18; then A500: 0+2<=(i+1)-'len h11 +2 by AXIOMS:24; then A501: 2-'1<=((i+1)-'len h11 +2-'1) by JORDAN3:5; (i+1)-len h11<=len h1+(len h2-2)-len h11 by A47,A458,REAL_1:49; then (i+1)-len h11<=(len h2-2) by A21,XCMPLX_1:26; then (i+1)-'len h11+2<=len h2-2+2 by A490,AXIOMS:24; then A502: (i+1)-'len h11+2<=len h2 by XCMPLX_1:27; then A503:1<=((i+1)-'len h11 +2-'1) & ((i+1)-'len h11 +2-'1)<=len h21 by A23,A500,Lm2,JORDAN3:5,7; A504:(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A501,Lm2,JORDAN3:1; set j=(i+1)-'len h11+2-'1; (i+1)-len h11<len h11+(len h2-2)-len h11 by A21,A47,A458,REAL_1:54; then (i+1)-len h11<len h2-2 by XCMPLX_1:26; then (i+1)-len h11+2<len h2-2+2 by REAL_1:53; then A505:(i+1)-len h11+2<len h2 by XCMPLX_1:27; A506:j+1=(i+1)-'len h11+(1+1)-1+1 by A501,Lm2,JORDAN3:1 .=(i+1)-'len h11+1+1-1+1 by XCMPLX_1:1 .=(i+1)-'len h11+1+1 by XCMPLX_1:26 .=(i+1)-'len h11+(1+1) by XCMPLX_1:1 .=(i+1)-'len h11+2; A507:j+1=1+((i+1)-len h11+(2-1)) by A490,A504,XCMPLX_1:29 .=1+((i+1)+-len h11+(2-1)) by XCMPLX_0:def 8 .=((i+1)+1)+-len h11+(2-1) by XCMPLX_1:1 .=(i+1)+1-len h11+(2-1) by XCMPLX_0:def 8 .=(i+1)+1-len h11+2-1 by XCMPLX_1:29 .=(i+1)+1-'len h11+2-'1 by A495,A499,BINARITH:def 3; A508: j in dom h2 by A22,A503,FINSEQ_3:27; then A509:h0.(i+1)=g2.(h2.j) by A492,FUNCT_1:23; A510: h2.j in rng h2 by A508,FUNCT_1:def 5; then A511:0<=h2.j & h2.j<=1 by A16,BORSUK_1:83,TOPREAL5:1; A512:j<j+1 by NAT_1:38; 1<j+1 by A501,Lm2,NAT_1:38; then A513:j+1 in dom h2 by A502,A506,FINSEQ_3:27; then A514:h0.((i+1)+1)=g2.(h2.(j+1)) & h21.(j+1)=g2.(h2.(j+1)) by A498,A507,FUNCT_1:23; A515: h2.(j+1) in rng h2 by A513,FUNCT_1:def 5; A516:h2.j<h2.(j+1) by A16,A508,A512,A513,GOBOARD1:def 1; i+1 in dom h0 by A458,A460,FINSEQ_3:27; then A517:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; (i+1)+1 in dom h0 by A459,A461,FINSEQ_3:27; then A518:h0/.((i+1)+1)=h0.((i+1)+1) by FINSEQ_4:def 4; A519:h0.(i+1) in Lower_Arc(P) by A13,A15,A16,A509,A510,BORSUK_1:83,FUNCT_1:def 5; A520:h0.((i+1)+1) in Lower_Arc(P) by A13,A15,A16,A514,A515,BORSUK_1:83,FUNCT_1:def 5; A521: 0 <= (h2.(j+1)) by A16,A515,BORSUK_1:83,TOPREAL5:1; A522: (h2.(j+1)) <= 1 by A16,A515,BORSUK_1:83,TOPREAL5:1; A523: h0/.(i+1+1) <> W-min P by A22,A29,A31,A65,A490,A498,A505,A506,A507,A513,A518,FUNCT_1:def 8; A524:i+1+1=i+(1+1) by XCMPLX_1:1; LE h0/.(i+1),h0/.((i+1)+1),Lower_Arc(P),E-max(P),W-min(P) by A11,A12,A13,A14,A509,A511,A514,A516,A517,A518, A521,A522,Th19; hence thesis by A517,A518,A519,A520,A523,A524,JORDAN6:def 10; case A525:i+1=len h1; then A526:h0.len h1 =E-max(P) by A21,A37,A460,SCMFSA_7:9; A527:len h1-len h11=len h1-'len h11 by A21,SCMFSA_7:3; A528: len h1+1 <=len h11 + len (mid(h21,2,len h21 -'1)) by A459,A525,FINSEQ_1:35; A529:h0.((i+1)+1)=(mid(h21,2,len h21 -'1)).((i+1)+1 -len h11) by A21,A40,A459,A525,FINSEQ_1:36; A530:(i+1)+1-len h11=(i+1)+1-'len h11 by A21,A462,A525,SCMFSA_7:3; (i+1)+1-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A525,A528,REAL_1:49; then A531:1<=(i+1)+1-'len h11 & (i+1)+1-'len h11<=len mid(h21,2,len h21 -'1) by A21,A525,A530,XCMPLX_1:26; then A532:h0.((i+1)+1)=h21.((i+1)+1-'len h11 +2-'1) by A43,A44,A529,A530,JORDAN3:27; 1<(i+1)+1-'len h11+(2-1) by A531,NAT_1:38; then 1<(i+1)+1-'len h11+2-1 by XCMPLX_1:29; then 0<(i+1)+1-'len h11+2-1 by AXIOMS:22; then A533:(i+1)+1-'len h11+2-1=(i+1)+1-'len h11+2-'1 by BINARITH:def 3; 0<=(i+1)-'len h11 by NAT_1:18; then 0+2<=(i+1)-'len h11 +2 by AXIOMS:24; then A534:2-'1<=((i+1)-'len h11 +2-'1) by JORDAN3:5; (i+1)-len h11<=len h1+(len h2-2)-len h11 by A47,A458,REAL_1:49; then (i+1)-'len h11<=len h2-2 by A21,A525,A527,XCMPLX_1:26; then (i+1)-'len h11+2<=len h2-2+2 by AXIOMS:24; then A535: (i+1)-'len h11+2<=len h2 by XCMPLX_1:27; A536:(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A534,Lm2,JORDAN3:1; set j=(i+1)-'len h11+2-'1; A537:0<=(i+1)-len h11 by A21,A525,XCMPLX_1:14; (i+1)-len h11<len h11+(len h2-2)-len h11 by A21,A47,A458,REAL_1:54; then (i+1)-len h11<len h2-2 by XCMPLX_1:26; then (i+1)-len h11+2<len h2-2+2 by REAL_1:53; then A538:(i+1)-len h11+2<len h2 by XCMPLX_1:27; A539:j+1=(i+1)-'len h11+(1+1)-1+1 by A534,Lm2,JORDAN3:1 .=(i+1)-'len h11+1+1-1+1 by XCMPLX_1:1 .=(i+1)-'len h11+1+1 by XCMPLX_1:26 .=(i+1)-'len h11+(1+1) by XCMPLX_1:1; then A540:j+1<len h2 by A537,A538,BINARITH:def 3; A541:j+1=(i+1)-len h11+2-1+1 by A536,A537,BINARITH:def 3 .=1+((i+1)-len h11+(2-1)) by XCMPLX_1:29 .=1+((i+1)+-len h11+(2-1)) by XCMPLX_0:def 8 .=((i+1)+1)+-len h11+(2-1) by XCMPLX_1:1 .=(i+1)+1-len h11+(2-1) by XCMPLX_0:def 8 .=(i+1)+1-'len h11+2-'1 by A530,A533,XCMPLX_1:29; 1<j+1 by A534,Lm2,NAT_1:38; then A542:j+1 in dom h2 by A535,A539,FINSEQ_3:27; then A543:h0.((i+1)+1)=g2.(h2.(j+1)) & h21.(j+1)=g2.(h2.(j+1)) by A532,A541,FUNCT_1:23; A544: h2.(j+1) in rng h2 by A542,FUNCT_1:def 5; len h1 in dom h0 by A458,A460,A525,FINSEQ_3:27; then A545:h0/.len h1=h0.len h1 by FINSEQ_4:def 4; (i+1)+1 in dom h0 by A459,A461,FINSEQ_3:27; then A546:h0/.((i+1)+1)=h0.((i+1)+1) by FINSEQ_4:def 4; A547:h0.(i+1+1) in Lower_Arc P by A13,A15,A16,A543,A544,BORSUK_1:83,FUNCT_1:def 5; A548: h0.(i+1) in Upper_Arc(P) by A1,A525,A526,Th1; A549: h0/.(i+1+1) <> W-min P by A22,A29,A31,A65,A532,A540,A541,A542,A546,FUNCT_1:def 8; i+1+1=i+(1+1) by XCMPLX_1:1 .=i+2; hence thesis by A525,A545,A546,A547,A548,A549,JORDAN6:def 10; end; hence thesis; end; hence thesis; end; A550: for i being Nat st 1<=i & i+1<=len h0 holds LE h0/.i,h0/.(i+1),P & h0/.(i+1)<>W-min(P) & h0/.i<>h0/.(i+1) proof let i be Nat such that A551: 1<=i and A552: i+1<=len h0; A553: 1<i+1 by A551,NAT_1:38; A554: i<len h0 by A552,NAT_1:38; A555: i<i+1 by NAT_1:38; i in dom h0 by A551,A554,FINSEQ_3:27; then A556: h0/.i=h0.i by FINSEQ_4:def 4; i+1 in dom h0 by A552,A553,FINSEQ_3:27; then A557: h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; now per cases; case A558:i<len h1; then A559:i+1<=len h1 by NAT_1:38; A560:h0.i=h11.i by A21,A551,A558,SCMFSA_7:9; A561:i in dom h1 by A551,A558,FINSEQ_3:27; then A562: h1.i in rng h1 by FUNCT_1:def 5; A563:h0.(i+1)=h11.(i+1) by A21,A553,A559,SCMFSA_7:9; A564:i+1 in dom h1 by A553,A559,FINSEQ_3:27; then A565:h0.(i+1)=g1.(h1.(i+1)) by A563,FUNCT_1:23; A566: h1.(i+1) in rng h1 by A564,FUNCT_1:def 5; A567:h1.i<h1.(i+1) by A9,A555,A561,A564,GOBOARD1:def 1; g1.(h1.i) in rng g1 by A6,A9,A562,BORSUK_1:83,FUNCT_1:def 5; then A568:h0.i in Upper_Arc(P) by A4,A560,A561,FUNCT_1:23; A569:h0.(i+1) in Upper_Arc(P) by A4,A6,A9,A565,A566,BORSUK_1:83,FUNCT_1:def 5; A570: g1.(h1.i) = h0/.i by A556,A560,A561,FUNCT_1:23; A571: 0 <= (h1.i) by A9,A562,BORSUK_1:83,TOPREAL5:1; A572: (h1.i) <= 1 by A9,A562,BORSUK_1:83,TOPREAL5:1; A573: 0 <= (h1.(i+1)) by A9,A566,BORSUK_1:83,TOPREAL5:1; A574: (h1.(i+1)) <= 1 by A9,A566,BORSUK_1:83,TOPREAL5:1; A575: i+1 <> 1 by A551,NAT_1:38; A576: i+1 <> i by NAT_1:38; LE h0/.i,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A2,A3,A4,A5,A557,A565,A567,A570,A571,A572,A573,A574,Th19 ; hence thesis by A20,A25,A38,A64,A556,A557,A560,A561,A563,A564, A568,A569,A575,A576,FUNCT_1:def 8,JORDAN6:def 10; case A577: i>=len h1; now per cases by A577,REAL_1:def 5; case A578:i>len h1; then A579:len h1 +1<=i by NAT_1:38; A580:len h11+1<=i & i<=len h11 + len (mid(h21,2,len h21 -'1)) by A21,A554,A578,FINSEQ_1:35,NAT_1:38; then A581: h0.i=(mid(h21, 2,len h21 -'1)).(i -len h11) by FINSEQ_1:36; A582:i-len h11=i-'len h11 by A21,A578,SCMFSA_7:3; A583: i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A580,REAL_1:49; len h1 +1-len h1<=i-len h1 by A579,REAL_1:49; then 1<=i-'len h11 & i-'len h11<=len mid(h21,2,len h21 -'1) by A21,A582,A583,XCMPLX_1:26; then A584:h0.i=h21.(i-'len h11 +2-'1) by A43,A44,A581,A582,JORDAN3:27; A585:len h1 +1<=i+1 by A579,NAT_1:38; then A586:h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A21,A40,A552,FINSEQ_1:36; i+1>len h11 by A21,A578,NAT_1:38; then A587:i+1-len h11=i+1-'len h11 by SCMFSA_7:3; A588: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A552,REAL_1:49; len h1 +1-len h1<=i+1-len h1 by A585,REAL_1:49; then A589: 1<=i+1-'len h11 & i+1-'len h11<=len mid(h21,2,len h21 -' 1) by A21,A587,A588,XCMPLX_1:26; then A590:h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A43,A44,A586,A587,JORDAN3:27; 1<i+1-'len h11+(2-1) by A589,NAT_1:38; then 1<i+1-'len h11+2-1 by XCMPLX_1:29; then 0<i+1-'len h11+2-1 by AXIOMS:22; then A591:i+1-'len h11+2-1=i+1-'len h11+2-'1 by BINARITH:def 3; 0<=i-'len h11 by NAT_1:18; then A592: 0+2<=i-'len h11 +2 by AXIOMS:24; then A593: 2-'1<=(i-'len h11 +2-'1) by JORDAN3:5; i-len h11<=len h1+(len h2-2)-len h11 by A47,A554,REAL_1:49; then i-len h11<=(len h2-2) by A21,XCMPLX_1:26; then i-'len h11+2<=len h2-2+2 by A582,AXIOMS:24; then A594: i-'len h11+2<=len h2 by XCMPLX_1:27; A595: 1<=i-'len h11 +2-'1 by A592,Lm2,JORDAN3:5; A596: i-'len h11 +2-'1<=len h21 by A23,A594,JORDAN3:7; set j=i-'len h11+2-'1; i-len h11<len h11+(len h2-2)-len h11 by A21,A47,A554,REAL_1:54; then i-len h11<len h2-2 by XCMPLX_1:26; then A597: i-len h11+2<len h2-2+2 by REAL_1:53; j+1=i-'len h11+(1+1)-1+1 by A593,Lm2,JORDAN3:1 .=i-'len h11+1+1-1+1 by XCMPLX_1:1 .=i-'len h11+1+1 by XCMPLX_1:26 .=i-'len h11+(1+1) by XCMPLX_1:1; then A598:j+1<len h2 by A582,A597,XCMPLX_1:27; A599:j+1=i-len h11+2-1+1 by A582,A593,Lm2,JORDAN3:1 .=1+(i-len h11+(2-1)) by XCMPLX_1:29 .=1+(i+-len h11+(2-1)) by XCMPLX_0:def 8 .=(i+1)+-len h11+(2-1) by XCMPLX_1:1 .=i+1-len h11+(2-1) by XCMPLX_0:def 8 .=i+1-'len h11+2-'1 by A587,A591,XCMPLX_1:29; A600:j in dom h2 by A22,A595,A596,FINSEQ_3:27; then A601:h0.i=g2.(h2.j) by A584,FUNCT_1:23; A602: h2.j in rng h2 by A600,FUNCT_1:def 5; A603:j<j+1 by NAT_1:38; 1<j+1 by A595,NAT_1:38; then A604:j+1 in dom h2 by A598,FINSEQ_3:27; then A605:h0.(i+1)=g2.(h2.(j+1)) & h21.(j+1)=g2.(h2.(j+1)) by A590,A599,FUNCT_1:23; A606: h2.(j+1) in rng h2 by A604,FUNCT_1:def 5; A607: h2.j<h2.(j+1) by A16,A600,A603,A604,GOBOARD1:def 1; i in dom h0 by A551,A554,FINSEQ_3:27; then A608:h0/.i=h0.i by FINSEQ_4:def 4; i+1 in dom h0 by A552,A553,FINSEQ_3:27; then A609:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; A610: 0 <= (h2.j) by A16,A602,BORSUK_1:83,TOPREAL5:1; A611: (h2.j) <= 1 by A16,A602,BORSUK_1:83,TOPREAL5:1; A612: 0 <= (h2.(j+1)) by A16,A606,BORSUK_1:83,TOPREAL5:1; A613: (h2.(j+1)) <= 1 by A16,A606,BORSUK_1:83,TOPREAL5:1; A614: h0/.(i+1) <> W-min P by A22,A29,A31,A65,A590,A598,A599,A604,A609,FUNCT_1:def 8; A615: j < j+1 by NAT_1:38; h0/.i in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P) & LE h0/.i,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A11,A12,A13,A14,A15,A16,A601, A602,A605,A606,A607,A608,A609,A610,A611,A612,A613,Th19,BORSUK_1:83,FUNCT_1:def 5; hence thesis by A22,A65,A584,A590,A599,A600,A604,A608,A609, A614,A615,FUNCT_1:def 8,JORDAN6:def 10; case A616:i=len h1; then A617:h0.i=E-max(P) by A21,A37,A551,SCMFSA_7:9; A618:i-len h11=i-'len h11 by A21,A616,SCMFSA_7:3; A619: i+1 <=len h11 + len (mid(h21,2,len h21 -'1)) by A552,FINSEQ_1:35; A620:h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A21,A40,A552,A616,FINSEQ_1:36; A621:i+1-len h11=i+1-'len h11 by A21,A555,A616,SCMFSA_7:3; A622: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A619,REAL_1:49; A623: 1<=i+1-'len h11 by A21,A616,A621,XCMPLX_1:26; i+1-'len h11<= len mid(h21,2,len h21 -'1) by A621,A622,XCMPLX_1:26; then A624:h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A43,A44,A620,A621,A623,JORDAN3:27; 1<i+1-'len h11+(2-1) by A623,NAT_1:38; then 1<i+1-'len h11+2-1 by XCMPLX_1:29; then 0<i+1-'len h11+2-1 by AXIOMS:22; then A625:i+1-'len h11+2-1=i+1-'len h11+2-'1 by BINARITH:def 3; 0<=i-'len h11 by NAT_1:18; then A626: 0+2<=i-'len h11 +2 by AXIOMS:24; then A627:2-'1<=(i-'len h11 +2-'1) by JORDAN3:5; i-len h11<=len h1+(len h2-2)-len h11 by A47,A554,REAL_1:49; then i-'len h11<=len h2-2 by A21,A618,XCMPLX_1:26; then A628: i-'len h11+2<=len h2-2+2 by AXIOMS:24; then i-'len h11+2<=len h2 by XCMPLX_1:27; then A629:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21 by A23,A626,Lm2,JORDAN3:5,7; A630:i-'len h11+2-'1=i-'len h11+2-1 by A627,Lm2,JORDAN3:1; set j=i-'len h11+2-'1; len h1-len h11>=0 by A21,XCMPLX_1:14; then len h1-'len h11=len h11-len h11 by A21,BINARITH:def 3; then A631: 0+2-1=len h1-'len h11+2-1 by XCMPLX_1:14; A632:0<=i-len h11 by A21,A616,XCMPLX_1:14; i-len h11<len h11+(len h2-2)-len h11 by A21,A47,A554,REAL_1:54; then i-len h11<len h2-2 by XCMPLX_1:26; then i-len h11+2<len h2-2+2 by REAL_1:53; then A633:i-len h11+2<len h2 by XCMPLX_1:27; A634:j+1=i-'len h11+(1+1)-1+1 by A627,Lm2,JORDAN3:1 .=i-'len h11+1+1-1+1 by XCMPLX_1:1 .=i-'len h11+1+1 by XCMPLX_1:26 .=i-'len h11+(1+1) by XCMPLX_1:1 .=i-'len h11+2; then A635:j+1<=len h2 by A628,XCMPLX_1:27; A636:j+1<len h2 by A632,A633,A634,BINARITH:def 3; A637:j+1=i-len h11+2-1+1 by A630,A632,BINARITH:def 3 .=1+(i-len h11+(2-1)) by XCMPLX_1:29 .=1+(i+-len h11+(2-1)) by XCMPLX_0:def 8 .=(i+1)+-len h11+(2-1) by XCMPLX_1:1 .=i+1-len h11+(2-1) by XCMPLX_0:def 8 .=i+1-'len h11+2-'1 by A621,A625,XCMPLX_1:29; A638:j in dom h2 by A22,A629,FINSEQ_3:27; then A639:h21.j=g2.(h2.j) by FUNCT_1:23; A640:h0.i=g2.(h2.j) by A14,A16,A616,A617,A631,JORDAN3:1; 1<j+1 by A627,Lm2,NAT_1:38; then A641:j+1 in dom h2 by A635,FINSEQ_3:27; then A642:h0.(i+1)=g2.(h2.(j+1)) by A624,A637,FUNCT_1:23; A643: h2.(j+1) in rng h2 by A641,FUNCT_1:def 5; i in dom h0 by A551,A554,FINSEQ_3:27; then A644:h0/.i=h0.i by FINSEQ_4:def 4; i+1 in dom h0 by A552,A553,FINSEQ_3:27; then A645:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; A646:h0.(i+1) in Lower_Arc(P) by A13,A15,A16,A642,A643,BORSUK_1:83,FUNCT_1:def 5; A647: h0.i in Upper_Arc(P) by A1,A617,Th1; A648: h0/.(i+1) <> W-min P by A22,A29,A31,A65,A624,A636,A637,A641,A645,FUNCT_1:def 8; j+1 <> j by NAT_1:38; hence thesis by A22,A65,A624,A637,A638,A639,A640,A641,A644,A645,A646,A647, A648,FUNCT_1:def 8,JORDAN6:def 10; end; hence thesis; end; hence thesis; end; thus for i being Nat st 1<=i & i+1<len h0 holds Segment(h0/.i,h0/.(i+1),P)/\ Segment(h0/.(i+1),h0/.(i+2),P) ={h0/.(i+1)} proof let i be Nat;assume A649: 1<=i & i+1<len h0; then A650:LE h0/.i,h0/.(i+1),P & h0/.(i+1)<>W-min(P) & h0/.i<>h0/.(i+1) by A550; A651: LE h0/.(i+1),h0/.(i+2),P by A457,A649; then h0/.i<>h0/.(i+2) by A1,A650,JORDAN6:72; hence Segment(h0/.i,h0/.(i+1),P)/\ Segment(h0/.(i+1),h0/.(i+2),P) ={h0/.(i+1)} by A1,A650,A651,Th10; end; thus Segment(h0/.len h0,h0/.1,P)/\ Segment(h0/.1,h0/.2,P)={h0/.1} proof A652: h11.2 <> W-min(P) by A20,A25,A38,A57,A64,FUNCT_1:def 8; A653:h0.2=g1.(h1.2) by A57,A60,FUNCT_1:23; A654: h1.2 in rng h1 by A57,FUNCT_1:def 5; A655:h0/.2=h0.2 by A59,FINSEQ_4:def 4; then A656: h0/.2 in Upper_Arc P by A4,A6,A9,A653,A654,BORSUK_1:83,FUNCT_1:def 5; len h1 +1-len h1<=len h0 -len h1 by A48,REAL_1:49; then A657: 1<=len h0 -len h1 by XCMPLX_1:26; A658:h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11) by A21,A40,A48,FINSEQ_1:36; len h0 -len h11 <=len h11 + len mid(h21,2,len h21 -'1) -len h11 by FINSEQ_1:35; then len h0-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; then A659:h0.len h0=h21.(len h0-'len h11 +2-'1) by A21,A43,A44,A54,A657,A658,JORDAN3:27; 0<=len h0-'len h11 by NAT_1:18; then A660: 0+2<=len h0-'len h11 +2 by AXIOMS:24; len h0-'len h11+2<=len h2-2+2 by A21,A47,A54,XCMPLX_1:26; then len h0-'len h11+2<=len h2 by XCMPLX_1:27; then A661:1<=(len h0-'len h11 +2-'1) & (len h0-'len h11 +2-'1)<=len h21 by A23,A660,Lm2,JORDAN3:5,7; set j=len h0-'len h11+2-'1; A662:j in dom h2 by A22,A661,FINSEQ_3:27; then A663:h0.len h0=g2.(h2.j) by A659,FUNCT_1:23; A664: now assume A665:h0/.2=h0/.len h0; h2.j in rng h2 by A662,FUNCT_1:def 5; then g2.(h2.j) in rng g2 by A15,A16,BORSUK_1:83,FUNCT_1:def 5; then h0/.2 in Upper_Arc(P)/\ Lower_Arc(P) by A13,A52,A656,A663,A665,XBOOLE_0:def 3; then h0/.2 in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; then h11.2=E-max(P) by A60,A652,A655,TARSKI:def 2; hence contradiction by A20,A35,A37,A56,A57,A64,FUNCT_1:def 8; end; defpred P[Nat] means $1+2<=len h0 implies LE h0/.2,h0/.($1+2),P; Upper_Arc(P) \/ Lower_Arc(P)= P by A1,JORDAN6:65; then h0/.2 in P by A656,XBOOLE_0:def 2; then A666: P[0] by A1,JORDAN6:71; A667:for k being Nat st P[k] holds P[k+1] proof let k be Nat;assume A668: k+2<=len h0 implies LE h0/.2,h0/.(k+2),P; now assume A669:k+1+2<=len h0; A670:k+1+2=k+2+1 by XCMPLX_1:1; then A671:k+2<len h0 by A669,NAT_1:38; A672:1<=1+k by NAT_1:29; k+1+1=k+(1+1) by XCMPLX_1:1 .=k+2; then LE h0/.(k+2),h0/.(k+2+1),P by A457,A670,A671,A672; hence LE h0/.2,h0/.(k+1+2),P by A1,A668,A669,A670,JORDAN6:73,NAT_1:38; end; hence (k+1+2<=len h0 implies LE h0/.2,h0/.(k+1+2),P); end; A673:for i being Nat holds P[i] from Ind(A666,A667); len h0 -'2=len h0-2 by A58,SCMFSA_7:3; then len h0-'2+2=len h0 by XCMPLX_1:27; then LE h0/.2,h0/.len h0,P & h0/.2<>h0/.len h0 & h0/.2<>W-min(P) by A59,A60,A652,A664,A673,FINSEQ_4: def 4; hence thesis by A1,A63,Th12; end; set i = len h0-'1; A674: i+1 = len h0 by A50,AMI_5:4; A675: 1<=i by A58,Lm4; A676: len h0 > 1+1+1 by A122,AXIOMS:22; then A677: len h0-'1 > 1+1 by Lm3; A678: i<len h0 by A50,JORDAN5B:1; then A679: i in dom h0 by A675,FINSEQ_3:27; then A680:h0/.i=h0.i by FINSEQ_4:def 4; A681:i+1<=len h0 by A678,NAT_1:38; A682:1+1<=len h0 by A50,NAT_1:38; A683:LE h0/.i,h0/.(i+1),P by A550,A675,A681; A684:LE h0/.1,h0/.(1+1),P by A550,A682; 1+1 in dom h0 by A682,FINSEQ_3:27; then A685:h0/.(1+1)=h0.(1+1) by FINSEQ_4:def 4; A686:h0/.1<>h0/.(1+1) by A550,A682; A687:h0.(1+1)=h11.(1+1) by A21,A56,SCMFSA_7:9; A688: 1+1 in dom h1 by A56,FINSEQ_3:27; then A689:h0.(1+1)=g1.(h1.(1+1)) by A687,FUNCT_1:23; A690: h1.(1+1) in rng h1 by A688,FUNCT_1:def 5; A691:1<i by A677,AXIOMS:22; A692: now per cases; case A693:i<=len h1; then A694:h0.i=h11.i by A21,A691,SCMFSA_7:9; A695:i in dom h1 by A691,A693,FINSEQ_3:27; then A696:h1.(1+1)<h1.i by A9,A677,A688,GOBOARD1:def 1; A697: h1.i in rng h1 by A695,FUNCT_1:def 5; A698:h0.i=g1.(h1.i) by A694,A695,FUNCT_1:23; A699:0<=h1.i & h1.i<=1 by A9,A697,BORSUK_1:83,TOPREAL5:1; 0 <= h1.(1+1) & h1.(1+1) <= 1 by A9,A690,BORSUK_1:83,TOPREAL5:1; then h0/.(1+1) in Upper_Arc(P) & h0/.i in Upper_Arc(P) & LE h0/.(1+1),h0/.i,Upper_Arc(P),W-min(P),E-max(P) by A2,A3,A4,A5,A6,A9,A680,A685,A689,A690,A696,A697,A698,A699, Th19,BORSUK_1:83,FUNCT_1:def 5; hence LE h0/.(1+1),h0/.i,P by JORDAN6:def 10; case A700:i>len h1; then A701:i-len h11=i-'len h11 by A21,SCMFSA_7:3; i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A678,REAL_1:49; then A702:0<=i-'len h11 & i-'len h11<=len mid(h21,2,len h21 -'1) by A21,A700,A701,SQUARE_1:12,XCMPLX_1:26; i-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A678,REAL_1:49; then A703:i-len h11 <= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; 0+1<=i-'len h11+1 by A702,AXIOMS:24; then 0+1<=i-'len h11+1+1-1 by XCMPLX_1:26; then 0+1<=i-'len h11+(1+1)-1 by XCMPLX_1:1; then A704:i-'len h11+2-'1=i-'len h11+2-1 by JORDAN3:1; 0<=i-'len h11 by NAT_1:18; then 0+2<=i-'len h11 +2 by AXIOMS:24; then A705:2-'1<=(i-'len h11 +2-'1) by JORDAN3:5; i-len h11<=len h1+(len h2-2)-len h11 by A47,A678,REAL_1:49; then i-'len h11<=len h2-2 by A21,A701,XCMPLX_1:26; then i-'len h11+2<=len h2-2+2 by AXIOMS:24; then i-'len h11+2<=len h2 by XCMPLX_1:27; then i-'len h11 +2-'1<=len h21 by A23,JORDAN3:7; then A706: (i-'len h11 +2-'1) in dom h21 by A705,Lm2,FINSEQ_3:27; 1+1 in dom h1 by A56,FINSEQ_3:27; then A707: h11.(1+1)=g1.(h1.(1+1)) by FUNCT_1:23; A708:len h1 +1<=i by A700,NAT_1:38; then A709:h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A21,A40,A678,FINSEQ_1:36; len h1 +1-len h1<=i-len h1 by A708,REAL_1:49; then A710: 1<=i-len h11 by A21,XCMPLX_1:26; then A711:h0.(i)=h21.(i-'len h11 +2-'1) by A43,A44,A701,A703,A709,JORDAN3:27; i+1-1<=len h1+(len h2-2)-1 by A47,A681,REAL_1:49; then i<=len h1+(len h2-2)-1 by XCMPLX_1:26; then i-len h11<=len h1+(len h2-2)-1-len h11 by REAL_1:49; then i-len h11<=len h1+((len h2-2)-1)-len h11 by XCMPLX_1:29 ; then i-'len h11<=len h2-2-1 by A21,A701,XCMPLX_1:26; then i-'len h11+2<=len h2-2-1+2 by AXIOMS:24; then i-'len h11+2<=len h2-1 by XCMPLX_1:229; then A712:i-'len h11+2-1<=len h2-1-1 by REAL_1:49; set k=i-'len h11+2-'1; A713: h2.k in rng h2 by A22,A706,FUNCT_1:def 5; A714: h1.(1+1) in rng h1 by A57,FUNCT_1:def 5; A715:h0.i=h21.k by A43,A44,A701,A703,A709,A710,JORDAN3:27; A716:h0.i=g2.(h2.k) & h21.k=g2.(h2.k) by A22,A706,A711,FUNCT_1:23; A717:g1.(h1.(1+1)) in rng g1 by A6,A9,A714,BORSUK_1:83,FUNCT_1:def 5; A718:h0.i in Lower_Arc(P) by A13,A15,A16,A713,A716,BORSUK_1:83,FUNCT_1:def 5; h0/.i <> W-min P by A17,A22,A29,A31,A65,A680,A704,A706,A712,A715,FUNCT_1:def 8; hence LE h0/.(1+1),h0/.i,P by A4,A680,A685,A687,A707,A717,A718,JORDAN6:def 10; end; thus Segment(h0/.(len h0-' 1),h0/.len h0,P)/\ Segment(h0/.len h0,h0/.1,P) ={h0/.len h0} proof A719:LE h0/.i,h0/.(i+1),P & h0/.(i+1)<>W-min(P) & h0/.i<>h0/.(i+1) by A550,A674,A675; i <> 1 by A676,Lm3; then h0/.i <> h0/.1 by A61,A66,A679,PARTFUN2:17; hence Segment(h0/.i,h0/.len h0,P)/\ Segment(h0/.len h0,h0/.1,P)={h0/.len h0 } by A1,A63,A674,A719,Th11; end; now now assume A720:h0/.(1+1)=h0/.i; now A721:1+1 in dom h1 by A56,FINSEQ_3:27; then A722: h1.(1+1) in rng h1 by FUNCT_1:def 5; A723:h0.(1+1)=h11.(1+1) by A21,A56,SCMFSA_7:9; then h0.(1+1)=g1.(h1.(1+1)) by A721,FUNCT_1:23; then A724:h0.(1+1) in Upper_Arc(P) by A4,A6,A9,A722,BORSUK_1:83, FUNCT_1:def 5; now per cases; case A725:i<=len h1; then A726:h0.i=h11.i by A21,A675,SCMFSA_7:9; i in dom h1 by A675,A725,FINSEQ_3:27; hence contradiction by A20,A64,A677,A680,A685,A720,A721,A723,A726,FUNCT_1:def 8; case A727:i>len h1; then A728:len h1 +1<=i by NAT_1:38; then A729: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A21,A40,A678,FINSEQ_1:36; A730:i-len h11=i-'len h11 by A21,A727,SCMFSA_7:3; i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A678,REAL_1:49; then A731:i-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; len h1 +1-len h1<=i-len h1 by A728,REAL_1:49; then 1<=i-len h1 by XCMPLX_1:26; then A732:h0.i=h21.(i-'len h11 +2-'1) by A21,A43,A44,A729,A730,A731,JORDAN3:27; 0<=i-'len h11 by NAT_1:18; then A733: 0+2<=i-'len h11 +2 by AXIOMS:24; then A734:2-'1<=(i-'len h11 +2-'1) by JORDAN3:5; i-len h11<=len h1+(len h2-2)-len h11 by A47,A678,REAL_1:49; then i-'len h11<=len h2-2 by A21,A730,XCMPLX_1:26; then i-'len h11+2<=len h2-2+2 by AXIOMS:24; then i-'len h11+2<=len h2 by XCMPLX_1:27; then A735:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21 by A23,A733,Lm2,JORDAN3:5,7; A736:i-'len h11+2-'1=i-'len h11+2-1 by A734,Lm2,JORDAN3:1; set k=i-'len h11+2-'1; i-len h11<=len h1+(len h2-2)-len h11 by A47,A678,REAL_1:49; then i-'len h11<=len h2-2 by A21,A730,XCMPLX_1:26; then i-'len h11+2<=len h2-2+2 by AXIOMS:24; then A737:i-'len h11+2<=len h2 by XCMPLX_1:27; i-'len h11+2-'1<i-'len h11+2-1+1 by A736,NAT_1:38; then A738: i-'len h11+2-'1<i-'len h11+2 by XCMPLX_1:27; len h11+1-len h11<=i-len h11 by A21,A728,REAL_1:49; then 1<=i-len h11 by XCMPLX_1:26; then 1<=i-'len h11 by JORDAN3:1; then 1+2<=i-'len h11+2 by AXIOMS:24; then 1+2-1<=i-'len h11+2-1 by REAL_1:49; then A739:1<k by A736,AXIOMS:22; A740:k in dom h2 by A22,A735,FINSEQ_3:27; then A741:h0.i=g2.(h2.k) by A732,FUNCT_1:23; A742: h2.k in rng h2 by A740,FUNCT_1:def 5; i in dom h0 by A675,A678,FINSEQ_3:27; then A743:h0/.i=h0.i by FINSEQ_4:def 4; g2.(h2.k) in rng g2 by A15,A16,A742,BORSUK_1:83,FUNCT_1:def 5; then h0.i in Upper_Arc(P) /\ Lower_Arc(P) by A13,A685,A720,A724,A741,A743,XBOOLE_0:def 3; then h0.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; then h0.i=W-min(P) or h0.i=E-max(P)by TARSKI:def 2; hence contradiction by A22,A28,A29,A30,A31,A65,A732,A737,A738, A739,A740,FUNCT_1:def 8; end; hence contradiction; end; hence contradiction; end; hence Segment(h0/.1,h0/.(1+1),P) misses Segment(h0/.i,h0/.len h0,P) by A1,A674,A683,A684,A686,A692,Th13; end; hence Segment(h0/.i,h0/.len h0,P) misses Segment(h0/.1,h0/.2,P); thus for i,j being Nat st 1<=i & i < j & j < len h0 & not i,j are_adjacent1 holds Segment(h0/.i,h0/.(i+1),P) misses Segment(h0/.j,h0/.(j+1),P) proof let i,j be Nat;assume that A744: 1<=i and A745: i < j and A746: j < len h0 and A747: not i,j are_adjacent1; A748: i<len h0 by A745,A746,AXIOMS:22; A749: 1<j by A744,A745,AXIOMS:22; i in dom h0 by A744,A748,FINSEQ_3:27; then A750:h0/.i=h0.i by FINSEQ_4:def 4; A751:i+1<=len h0 by A748,NAT_1:38; A752:j+1<=len h0 by A746,NAT_1:38; A753:LE h0/.i,h0/.(i+1),P by A550,A744,A751; A754:LE h0/.j,h0/.(j+1),P by A550,A749,A752; A755:not(j=i+1 or i=j+1) by A747,GOBRD10:def 1; 1<j+1 by A749,NAT_1:38; then j+1 in dom h0 by A752,FINSEQ_3:27; then A756:h0/.(j+1)=h0.(j+1) by FINSEQ_4:def 4; now per cases; case i<j; then A757: i+1<=j by NAT_1:38; then A758:i+1<j by A755,REAL_1:def 5; A759:i+1<len h0 by A746,A757,AXIOMS:22; A760:h0/.i<>h0/.(i+1) by A550,A744,A751; A761:1<i+1 by A744,NAT_1:38; A762:1<=(i+1) & (i+1)<len h0 by A744,A746,A757,AXIOMS:22,NAT_1:38; A763:LE h0/.(i+1),h0/.j,P proof now per cases; case A764:i+1<=len h1; now per cases; case A765:j<=len h1; A766:h0.(i+1)=h11.(i+1) by A21,A762,A764,SCMFSA_7:9; A767:(i+1) in dom h1 by A762,A764,FINSEQ_3:27; then A768: h1.(i+1) in rng h1 by FUNCT_1:def 5; A769:1<j by A758,A762,AXIOMS:22; then A770:h0.j=h11.j by A21,A765,SCMFSA_7:9; A771:j in dom h1 by A765,A769,FINSEQ_3:27; then A772: h1.j in rng h1 by FUNCT_1:def 5; i+1 in dom h0 by A762,FINSEQ_3:27; then A773:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; j in dom h0 by A746,A769,FINSEQ_3:27; then h0/.j=h0.j by FINSEQ_4:def 4; then Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) & g1.(h1.(i+1)) = h0/.(i+1) & 0 <= (h1.(i+1)) & (h1.(i+1)) <= 1 & g1.(h1.j) = h0/.j & 0 <= (h1.j) & (h1.j) <= 1 & (h1.(i+1)) <= (h1.j) by A1,A9,A758,A766,A767,A768,A770,A771,A772,A773,BORSUK_1 :83,FUNCT_1:23,GOBOARD1:def 1,JORDAN6:def 8,TOPREAL5:1; then h0/.(i+1) in Upper_Arc(P) & h0/.j in Upper_Arc(P) & LE h0/.(i+1),h0/.j,Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A9,A768,A772,Th19, BORSUK_1:83,FUNCT_1:def 5; hence thesis by JORDAN6:def 10; case A774:j>len h1; then A775:len h11<=j & j<=len h11 + len (mid(h21,2,len h21 -'1)) by A20,A746,FINSEQ_1:35,FINSEQ_3:31; A776:j-len h11=j-'len h11 by A21,A774,SCMFSA_7:3; j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A775,REAL_1:49; then A777:0<=j-'len h11 & j-'len h11<=len mid(h21,2,len h21 -'1) by A21,A774,A776,SQUARE_1:12,XCMPLX_1:26; A778: j-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A746,REAL_1:49; then A779:j-len h11 <= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; 0+1<=j-'len h11+1 by A777,AXIOMS:24; then 0+1<=j-'len h11+1+1-1 by XCMPLX_1:26; then 0+1<=j-'len h11+(1+1)-1 by XCMPLX_1:1; then A780:j-'len h11+2-'1=j-'len h11+2-1 by JORDAN3:1; 0<=j-'len h11 by NAT_1:18; then 0+2<=j-'len h11 +2 by AXIOMS:24; then A781:2-'1<=j-'len h11 +2-'1 by JORDAN3:5; j-len h11<=len h1+(len h2-2)-len h11 by A47,A746,REAL_1:49; then j-len h11<=(len h2-2) by A21,XCMPLX_1:26; then j-'len h11+2<=len h2-2+2 by A776,AXIOMS:24; then j-'len h11+2<=len h2 by XCMPLX_1:27; then A782: (j-'len h11 +2-'1)<=len h21 by A23,JORDAN3:7; then A783:(j-'len h11 +2-'1) in dom h21 by A781,Lm2,FINSEQ_3: 27; i+1 in Seg len h1 by A762,A764,FINSEQ_1:3; then i+1 in dom h1 by FINSEQ_1:def 3; then A784: j-len h11=j-'len h11 & h0.(i+1)=h11.(i+1) & (j-'len h11 +2-'1) in dom h21 & j-'len h11+2-'1=j-'len h11+2-1 & j-len h11 <= len (mid(h21,2,len h21 -'1)) & (i+1) in dom h1 & h11.(i+1)=g1.(h1.(i+1)) by A21,A761,A764,A774,A778,A781,A782,Lm2,FINSEQ_3:27,FUNCT_1:23, JORDAN3:1,SCMFSA_7:3,9,XCMPLX_1:26; A785:len h1 +1<=j by A774,NAT_1:38; then A786:h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) by A21,A40,A746,FINSEQ_1:36; len h1 +1-len h1<=j-len h1 by A785,REAL_1:49; then A787: 1<=j-len h1 by XCMPLX_1:26; then A788:h0.j=h21.(j-'len h11 +2-'1) by A21,A43,A44,A776,A779,A786,JORDAN3:27; j+1-1<=len h1+(len h2-2)-1 by A47,A752,REAL_1:49; then j<=len h1+(len h2-2)-1 by XCMPLX_1:26; then j-len h11<=len h1+(len h2-2)-1-len h11 by REAL_1:49; then j-len h11<=len h1+((len h2-2)-1)-len h11 by XCMPLX_1:29 ; then j-len h11<=(len h2-2-1) by A21,XCMPLX_1:26; then j-'len h11+2<=len h2-2-1+2 by A776,AXIOMS:24; then j-'len h11+2<=len h2-1 by XCMPLX_1:229; then A789:j-'len h11+2-1<=len h2-1-1 by REAL_1:49; A790: len h2-1-1<len h2 by Lm5; set k=j-'len h11+2-'1; A791: h2.k in rng h2 by A22,A783,FUNCT_1:def 5; i+1 in dom h1 by A761,A764,FINSEQ_3:27; then A792: h1.(i+1) in rng h1 by FUNCT_1:def 5; A793: h0.j=h21.k by A21,A43,A44,A784,A786,A787,JORDAN3:27; A794:h0.j=g2.(h2.k) & h21.k=g2.(h2.k) by A22,A783,A788, FUNCT_1:23; (i+1) in dom h0 by A762,FINSEQ_3:27; then A795:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; j in dom h0 by A746,A749,FINSEQ_3:27; then A796:h0/.j=h0.j by FINSEQ_4:def 4; A797:g1.(h1.(i+1)) in rng g1 by A6,A9,A792,BORSUK_1:83, FUNCT_1:def 5; A798:h0.j in Lower_Arc(P) by A13,A15,A16,A791,A794,BORSUK_1:83,FUNCT_1:def 5; h0/.j <> W-min P by A22,A29,A31,A65,A780,A783,A789,A790,A793,A796,FUNCT_1:def 8 ; hence thesis by A4,A784,A795,A796,A797,A798,JORDAN6:def 10; end; hence thesis; case A799:i+1>len h1; then A800: len h1<j by A757,AXIOMS:22; then A801:j-len h11=j-'len h11 by A21,SCMFSA_7:3; j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A746,REAL_1:49; then A802:0<=j-'len h11 & j-'len h11<=len mid(h21,2,len h21 -'1) by A21,A800,A801,SQUARE_1:12,XCMPLX_1:26; A803: j-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A746,REAL_1:49; then A804:j-len h11 <= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; 0+1<=j-'len h11+1 by A802,AXIOMS:24; then 0+1<=j-'len h11+1+1-1 by XCMPLX_1:26; then 0+1<=j-'len h11+(1+1)-1 by XCMPLX_1:1; then A805:j-'len h11+2-'1=j-'len h11+2-1 by JORDAN3:1; 0<=j-'len h11 by NAT_1:18; then 0+2<=j-'len h11 +2 by AXIOMS:24; then A806:2-'1<=j-'len h11 +2-'1 by JORDAN3:5; j-len h11<=len h1+(len h2-2)-len h11 by A47,A746,REAL_1:49; then j-len h11<=len h2-2 by A21,XCMPLX_1:26; then j-'len h11+2<=len h2-2+2 by A801,AXIOMS:24; then j-'len h11+2<=len h2 by XCMPLX_1:27; then A807: (j-'len h11 +2-'1)<=len h21 by A23,JORDAN3:7; then A808:j-'len h11 +2-'1 in dom h21 by A806,Lm2,FINSEQ_3:27 ; A809:len h11+1<=i+1 & i+1<len h11 + len (mid(h21,2,len h21 -'1)) by A21,A759,A799,FINSEQ_1:35,NAT_1:38; A810: i+1-len h11<len h11 + len (mid(h21,2,len h21 -'1)) - len h11 by A40,A759,REAL_1:54; then A811:i+1-len h11<len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; len h1+1<=i+1 by A799,NAT_1:38; then len h1+1-len h1<=i+1-len h1 by REAL_1:49; then 1<=i+1-len h1 by XCMPLX_1:26; then A812:1<=i+1-'len h11 & i+1-'len h11=i+1-len h11 by A21,JORDAN3:1; A813: h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A809,FINSEQ_1:36 .=h21.(i+1-'len h11+2-'1) by A43,A44,A811,A812,JORDAN3:27; then A814: j-len h11=j-'len h11 & (i+1)-len h11=(i+1)-'len h11 & h0.(i+1)=h21.(i+1-'len h11+2-'1) & (j-'len h11 +2-'1) in dom h21 & len h11+1<=i+1 & i+1<=len h11 + len (mid(h21,2,len h21 -'1)) & j-'len h11+2-'1=j-'len h11+2-1 & j-len h11 <= len (mid(h21,2,len h21 -'1)) & i+1-len h11<len (mid(h21,2,len h21 -'1)) by A21,A759,A799,A800,A803,A806,A807,A810,Lm2,FINSEQ_1:35, FINSEQ_3:27,JORDAN3:1,NAT_1:38,SCMFSA_7:3,XCMPLX_1:26; len h1<j by A757,A799,AXIOMS:22; then A815:len h11+1<=j & j<=len h11 + len (mid(h21,2,len h21 -'1)) by A21,A746,FINSEQ_1:35,NAT_1:38; then A816:h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) by FINSEQ_1:36; len h1 +1-len h1<=j-len h1 by A21,A815,REAL_1:49 ; then A817: 1<=j-len h1 by XCMPLX_1:26; then A818:h0.j=h21.(j-'len h11 +2-'1) by A21,A43,A44,A801,A804,A816,JORDAN3:27; 0<=(i+1)-'len h11 by NAT_1:18; then A819: 0+2<=(i+1)-'len h11 +2 by AXIOMS:24; then A820:2-'1<=((i+1)-'len h11 +2-'1) by JORDAN3:5; (i+1)-len h11<=len h11+(len h2-2)-len h11 by A21,A47,A759,REAL_1:49; then (i+1)-len h11<=(len h2-2) by XCMPLX_1:26; then (i+1)-'len h11+2<=len h2-2+2 by A814,AXIOMS:24; then (i+1)-'len h11+2<=len h2 by XCMPLX_1:27; then A821:1<=((i+1)-'len h11 +2-'1) & ((i+1)-'len h11 +2-'1)<=len h21 by A23,A819,Lm2,JORDAN3:5,7; A822:(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A820,Lm2,JORDAN3:1; j+1-1<=len h1+(len h2-2)-1 by A47,A752,REAL_1:49 ; then j<=len h1+(len h2-2)-1 by XCMPLX_1:26; then j-len h11<=len h1+(len h2-2)-1-len h11 by REAL_1:49; then j-len h11<=len h1+((len h2-2)-1)-len h11 by XCMPLX_1:29 ; then j-len h11<=(len h2-2-1) by A21,XCMPLX_1:26; then j-'len h11+2<=len h2-2-1+2 by A801,AXIOMS:24; then j-'len h11+2<=len h2-1 by XCMPLX_1:229; then A823:j-'len h11+2-1<=len h2-1-1 by REAL_1:49; A824: len h2-1-1<len h2 by Lm5; set k=j-'len h11+2-'1; set j0=(i+1)-'len h11+2-'1; (i+1)-len h11<j-len h11 by A758,REAL_1:54; then (i+1)-'len h11+2<j-'len h11+2 by A814,REAL_1:53; then A825:j0<k by A805,A822,REAL_1:54; A826:h21.k=g2.(h2.k) by A22,A808,FUNCT_1:23; A827: h2.k in rng h2 by A22,A808,FUNCT_1:def 5; then A828:0<=h2.k & h2.k<=1 by A16,BORSUK_1:83,TOPREAL5:1; A829:j0 in dom h2 by A22,A821,FINSEQ_3:27; then A830:h0.(i+1)=g2.(h2.j0) by A813,FUNCT_1:23; A831: h2.j0 in rng h2 by A829,FUNCT_1:def 5; then A832:0<=h2.j0 & h2.j0<=1 by A16,BORSUK_1:83,TOPREAL5:1; A833:h2.(j0)<h2.(k) by A16,A22,A808,A825,A829,GOBOARD1:def 1; A834: h0.j=h21.(k) by A21,A43,A44,A814,A816,A817,JORDAN3:27; A835:h0.j=g2.(h2.k) & h21.k=g2.(h2.k) by A22,A808,A818, FUNCT_1:23; (i+1) in dom h0 by A762,FINSEQ_3:27; then A836:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; j in dom h0 by A746,A749,FINSEQ_3:27; then A837:h0/.j=h0.(j) by FINSEQ_4:def 4; A838:g2.(h2.j0) in rng g2 by A15,A16,A831,BORSUK_1:83,FUNCT_1 :def 5; A839:h0.(j) in Lower_Arc(P) by A13,A15,A16,A827,A835,BORSUK_1:83,FUNCT_1:def 5; A840: h0/.j <> W-min P by A22,A29,A31,A65,A805,A808,A823,A824,A834,A837,FUNCT_1:def 8; LE h0/.(i+1),h0/.j,Lower_Arc(P),E-max(P),W-min(P) by A11,A12,A13,A14,A818,A826,A828,A830,A832,A833,A836,A837 ,Th19; hence thesis by A13,A830,A836,A837,A838,A839,A840,JORDAN6:def 10; end; hence thesis; end; now assume A841:h0/.(i+1)=h0/.j; now per cases; case A842:i+1<=len h1; A843:1<i+1 by A744,NAT_1:38; then A844:i+1 in dom h1 by A842,FINSEQ_3:27; i+1 in dom h0 by A751,A843,FINSEQ_3:27; then A845:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; A846:h0.(i+1)=h11.(i+1) by A21,A842,A843,SCMFSA_7:9; then A847:h0.(i+1)=g1.(h1.(i+1)) by A844,FUNCT_1:23; h1.(i+1) in rng h1 by A844,FUNCT_1:def 5; then A848:h0.(i+1) in Upper_Arc(P) by A4,A6,A9,A847,BORSUK_1:83,FUNCT_1:def 5; now per cases; case A849:j<=len h1; then A850:h0.(j)=h11.(j) by A21,A749,SCMFSA_7:9; A851:j in dom h1 by A749,A849,FINSEQ_3:27; j in dom h0 by A746,A749,FINSEQ_3:27; then h0/.j=h0.j by FINSEQ_4:def 4; hence contradiction by A20,A64,A755,A841,A844,A845,A846,A850,A851 ,FUNCT_1:def 8; case A852:j>len h1; then A853:len h1 +1<=j by NAT_1:38; A854:len h11+1<=j & j<= len h11 + len (mid(h21,2,len h21 -'1)) by A21,A746,A852,FINSEQ_1:35,NAT_1:38; A855: h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) by A21,A40,A746,A853,FINSEQ_1:36; A856:j-len h11=j-'len h11 by A21,A852,SCMFSA_7:3; j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A854,REAL_1:49; then A857:j-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; len h1 +1-len h1<=j-len h1 by A853,REAL_1:49; then 1<=j-len h11 by A21,XCMPLX_1:26; then A858:h0.j=h21.(j-'len h11 +2-'1) by A43,A44,A855,A856,A857,JORDAN3:27; 0<=j-'len h11 by NAT_1:18; then A859: 0+2<=j-'len h11 +2 by AXIOMS:24; then A860:2-'1<=(j-'len h11 +2-'1) by JORDAN3:5; j-len h11<=len h1+(len h2-2)-len h11 by A47,A746,REAL_1:49; then j-'len h11<=len h2-2 by A21,A856,XCMPLX_1:26; then j-'len h11+2<=len h2-2+2 by AXIOMS:24; then j-'len h11+2<=len h2 by XCMPLX_1:27; then A861:1<=(j-'len h11 +2-'1) & (j-'len h11 +2-'1)<= len h21 by A23,A859,Lm2,JORDAN3:5,7; A862:j-'len h11+2-'1=j-'len h11+2-1 by A860,Lm2,JORDAN3:1; set k=j-'len h11+2-'1; j-len h11<=len h1+(len h2-2)-len h11 by A47,A746,REAL_1:49; then j-'len h11<=len h2-2 by A21,A856,XCMPLX_1:26; then j-'len h11+2<=len h2-2+2 by AXIOMS:24; then A863:j-'len h11+2<=len h2 by XCMPLX_1:27; j-'len h11+2-'1<j-'len h11+2-'1+1 by NAT_1:38; then A864: j-'len h11+2-'1<j-'len h11+2 by A862,XCMPLX_1:27; len h11+1-len h11<=j-len h11 by A21,A853,REAL_1:49 ; then 1<=j-len h11 by XCMPLX_1:26; then 1<=j-'len h11 by JORDAN3:1; then 1+2<=j-'len h11+2 by AXIOMS:24; then 1+2-1<=j-'len h11+2-1 by REAL_1:49; then A865:1<k by A862,AXIOMS:22; A866:k in dom h2 by A22,A861,FINSEQ_3:27; then A867:h0.j=g2.(h2.k) by A858,FUNCT_1:23; A868: h2.k in rng h2 by A866,FUNCT_1:def 5; j in dom h0 by A746,A749,FINSEQ_3:27; then A869:h0/.j=h0.j by FINSEQ_4:def 4; g2.(h2.k) in rng g2 by A15,A16,A868,BORSUK_1:83,FUNCT_1:def 5; then h0.j in Upper_Arc(P) /\ Lower_Arc(P) by A13,A841,A845,A848,A867,A869,XBOOLE_0:def 3; then A870: h0.j in {W-min(P),E-max(P)} by A1,JORDAN6: def 9; A871: h0.j <> W-min P by A22,A29,A31,A65,A858,A863,A864,A866,FUNCT_1:def 8; h0.j <> E-max P by A22,A28,A30,A65,A858,A865,A866,FUNCT_1:def 8; hence contradiction by A870,A871,TARSKI:def 2; end; hence contradiction; case A872:i+1>len h1; then A873:len h1 +1<=i+1 by NAT_1:38; then A874:h0.(i+1)=(mid(h21,2,len h21 -'1)).((i+1) -len h11) by A21,A40,A751,FINSEQ_1:36; A875:(i+1)-len h11=(i+1)-'len h11 by A21,A872,SCMFSA_7:3; (i+1)-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A751,REAL_1:49; then A876:(i+1)-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; len h1 +1-len h1<=(i+1)-len h1 by A873,REAL_1:49 ; then 1<=(i+1)-len h11 by A21,XCMPLX_1:26; then A877:h0.(i+1)=h21.((i+1)-'len h11 +2-'1) by A43,A44,A874,A875,A876,JORDAN3:27; 0<=(i+1)-'len h11 by NAT_1:18; then A878: 0+2<=(i+1)-'len h11 +2 by AXIOMS:24; then A879:2-'1<=((i+1)-'len h11 +2-'1) by JORDAN3:5; (i+1)-len h11<=len h1+(len h2-2)-len h11 by A47,A751,REAL_1:49; then (i+1)-len h11<=(len h2-2) by A21,XCMPLX_1:26; then (i+1)-'len h11+2<=len h2-2+2 by A875,AXIOMS:24; then (i+1)-'len h11+2<=len h2 by XCMPLX_1:27; then A880:1<=((i+1)-'len h11 +2-'1) & ((i+1)-'len h11 +2-'1)<=len h21 by A23,A878,Lm2,JORDAN3:5,7; A881:(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A879,Lm2,JORDAN3:1; set j0=(i+1)-'len h11+2-'1; len h11+1-len h11<=(i+1)-len h11 by A21,A873,REAL_1:49; then 1<=(i+1)-len h11 by XCMPLX_1:26; then A882:(i+1)-'len h11=(i+1)-len h11 by JORDAN3:1; A883:j0 in dom h2 by A22,A880,FINSEQ_3:27; 1<=i+1 by A744,NAT_1:38; then i+1 in dom h0 by A751,FINSEQ_3:27; then A884:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; A885:j>len h1 by A757,A872,AXIOMS:22; then A886:len h1 +1<=j by NAT_1:38; len h11+1<=j & j<= len h11 + len (mid(h21,2,len h21 -'1)) by A21,A746,A885,FINSEQ_1:35,NAT_1:38; then A887: h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) by FINSEQ_1:36; A888:j-len h11=j-'len h11 by A21,A885,SCMFSA_7:3; A889: j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A746,REAL_1:49; len h1 +1-len h1<=j-len h1 by A886,REAL_1:49; then 1<=j-'len h11 & j-'len h11<=len mid(h21,2,len h21 -'1) by A21,A888,A889,XCMPLX_1:26; then A890:h0.j=h21.(j-'len h11 +2-'1) by A43,A44,A887,A888,JORDAN3:27; 0<=j-'len h11 by NAT_1:18; then A891: 0+2<=j-'len h11 +2 by AXIOMS:24; then A892:2-'1<=(j-'len h11 +2-'1) by JORDAN3:5; j-len h11<=len h1+(len h2-2)-len h11 by A47,A746,REAL_1:49; then j-len h11<=len h2-2 by A21,XCMPLX_1:26; then j-'len h11+2<=len h2-2+2 by A888,AXIOMS:24; then j-'len h11+2<=len h2 by XCMPLX_1:27; then A893:1<=(j-'len h11 +2-'1) & (j-'len h11 +2-'1)<=len h21 by A23,A891,Lm2,JORDAN3:5,7; A894:j-'len h11+2-'1=j-'len h11+2-1 by A892,Lm2,JORDAN3:1; set k=j-'len h11+2-'1; len h11+1-len h11<=j-len h11 by A21,A886,REAL_1:49 ; then 1<=j-len h11 by XCMPLX_1:26; then j-'len h11=j-len h11 by JORDAN3:1; then i+1-'len h11<j-'len h11 by A758,A882,REAL_1:54; then i+1-'len h11+2<j-'len h11+2 by REAL_1:53; then A895:(i+1)-'len h11+2-'1<j-'len h11+2-'1 by A881,A894,REAL_1:54; A896:k in dom h2 by A22,A893,FINSEQ_3:27; j in dom h0 by A746,A749,FINSEQ_3:27; then h0/.j=h0.j by FINSEQ_4:def 4; hence contradiction by A22,A65,A841,A877,A883,A884,A890,A895,A896,FUNCT_1:def 8; end; hence contradiction; end; hence Segment(h0/.i,h0/.(i+1),P) misses Segment(h0/.j,h0/.(j+1),P) by A1,A753,A754,A760,A763,Th13; case A897: j<=i; A898:h0/.j<>h0/.(j+1) by A550,A749,A752; A899:1<j+1 by A749,NAT_1:38; A900:LE h0/.(j+1),h0/.i,P proof now per cases; case A901:j+1<=len h1; then A902:h0.(j+1)=h11.(j+1) by A21,A899,SCMFSA_7:9; now per cases; case i<=len h1; thus thesis by A745,A897; case A903:i>len h1; then A904:i-len h11=i-'len h11 by A21,SCMFSA_7:3; i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A748,REAL_1:49; then A905:0<=i-'len h11 & i-'len h11<=len mid(h21,2,len h21 -'1) by A21,A903,A904,SQUARE_1:12,XCMPLX_1:26; i-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A748,REAL_1:49; then A906:i-len h11 <= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; 0+1<=i-'len h11+1 by A905,AXIOMS:24; then 0+1<=i-'len h11+1+1-1 by XCMPLX_1:26; then 0+1<=i-'len h11+(1+1)-1 by XCMPLX_1:1; then A907:i-'len h11+2-'1=i-'len h11+2-1 by JORDAN3:1; 0<=i-'len h11 by NAT_1:18; then 0+2<=i-'len h11 +2 by AXIOMS:24; then A908:2-'1<=(i-'len h11 +2-'1) by JORDAN3:5; i-len h11<=len h1+(len h2-2)-len h11 by A47,A748,REAL_1:49; then i-'len h11<=len h2-2 by A21,A904,XCMPLX_1:26; then i-'len h11+2<=len h2-2+2 by AXIOMS:24; then i-'len h11+2<=len h2 by XCMPLX_1:27; then i-'len h11 +2-'1<=len h21 by A23,JORDAN3:7; then A909: (i-'len h11 +2-'1) in dom h21 by A908,Lm2,FINSEQ_3:27; j+1 in dom h1 by A899,A901,FINSEQ_3:27; then A910: h11.(j+1)=g1.(h1.(j+1)) by FUNCT_1:23; A911:len h1 +1<=i by A903,NAT_1:38; then A912:h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A21,A40,A748,FINSEQ_1:36; len h1 +1-len h1<=i-len h1 by A911,REAL_1:49; then A913: 1<=i-len h11 by A21,XCMPLX_1:26; then A914:h0.(i)=h21.(i-'len h11 +2-'1) by A43,A44,A904,A906,A912,JORDAN3:27; i+1-1<=len h1+(len h2-2)-1 by A47,A751,REAL_1:49; then i<=len h1+(len h2-2)-1 by XCMPLX_1:26; then i-len h11<=len h1+(len h2-2)-1-len h11 by REAL_1:49; then i-len h11<=len h1+((len h2-2)-1)-len h11 by XCMPLX_1:29 ; then i-'len h11<=len h2-2-1 by A21,A904,XCMPLX_1:26; then i-'len h11+2<=len h2-2-1+2 by AXIOMS:24; then i-'len h11+2<=len h2-1 by XCMPLX_1:229; then A915:i-'len h11+2-1<=len h2-1-1 by REAL_1:49; A916: len h2-1-1<len h2 by Lm5; set k=i-'len h11+2-'1; A917: h2.k in rng h2 by A22,A909,FUNCT_1:def 5; j+1 in dom h1 by A899,A901,FINSEQ_3:27; then A918: h1.(j+1) in rng h1 by FUNCT_1:def 5; A919:h0.i=h21.k by A43,A44,A904,A906,A912,A913,JORDAN3:27; A920:h0.i=g2.(h2.k) & h21.k=g2.(h2.k) by A22,A909,A914,FUNCT_1:23; A921:g1.(h1.(j+1)) in rng g1 by A6,A9,A918,BORSUK_1:83,FUNCT_1:def 5; A922:h0.i in Lower_Arc(P) by A13,A15,A16,A917,A920,BORSUK_1:83,FUNCT_1:def 5; h0/.i <> W-min P by A22,A29,A31,A65,A750,A907,A909,A915,A916,A919,FUNCT_1:def 8; hence thesis by A4,A750,A756,A902,A910,A921,A922,JORDAN6:def 10; end; hence thesis; case j+1>len h1; thus thesis by A745,A897; end; hence thesis; end; A923:1<j+1 by A749,NAT_1:38; now assume A924:h0/.(j+1)=h0/.i; now per cases; case A925:j+1<=len h1; then A926:j+1 in dom h1 by A923,FINSEQ_3:27; then A927: h1.(j+1) in rng h1 by FUNCT_1:def 5; A928:h0.(j+1)=h11.(j+1) by A21,A923,A925,SCMFSA_7:9; then h0.(j+1)=g1.(h1.(j+1)) by A926,FUNCT_1:23; then A929:h0.(j+1) in Upper_Arc(P) by A4,A6,A9,A927,BORSUK_1:83, FUNCT_1:def 5; now per cases; case A930:i<=len h1; then A931:h0.i=h11.i by A21,A744,SCMFSA_7:9; i in dom h1 by A744,A930,FINSEQ_3:27; hence contradiction by A20,A64,A750,A755,A756,A924,A926,A928,A931,FUNCT_1:def 8; case A932:i>len h1; then A933:len h1 +1<=i by NAT_1:38; then A934: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A21,A40,A748,FINSEQ_1:36; A935:i-len h11=i-'len h11 by A21,A932,SCMFSA_7:3; i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A40,A748,REAL_1:49; then A936:i-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; len h1 +1-len h1<=i-len h1 by A933,REAL_1:49; then 1<=i-len h1 by XCMPLX_1:26; then A937:h0.i=h21.(i-'len h11 +2-'1) by A21,A43,A44,A934,A935,A936,JORDAN3:27; 0<=i-'len h11 by NAT_1:18; then A938: 0+2<=i-'len h11 +2 by AXIOMS:24; then A939:2-'1<=(i-'len h11 +2-'1) by JORDAN3:5; i-len h11<=len h1+(len h2-2)-len h11 by A47,A748,REAL_1:49; then i-'len h11<=len h2-2 by A21,A935,XCMPLX_1:26; then i-'len h11+2<=len h2-2+2 by AXIOMS:24; then i-'len h11+2<=len h2 by XCMPLX_1:27; then A940:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21 by A23,A938,Lm2,JORDAN3:5,7; A941:i-'len h11+2-'1=i-'len h11+2-1 by A939,Lm2,JORDAN3:1; set k=i-'len h11+2-'1; i-len h11<=len h1+(len h2-2)-len h11 by A47,A748,REAL_1:49; then i-'len h11<=len h2-2 by A21,A935,XCMPLX_1:26; then i-'len h11+2<=len h2-2+2 by AXIOMS:24; then A942:i-'len h11+2<=len h2 by XCMPLX_1:27; i-'len h11+2-'1<i-'len h11+2-1+1 by A941,NAT_1:38; then A943: i-'len h11+2-'1<i-'len h11+2 by XCMPLX_1:27; len h11+1-len h11<=i-len h11 by A21,A933,REAL_1:49; then 1<=i-len h11 by XCMPLX_1:26; then 1<=i-'len h11 by JORDAN3:1; then 1+2<=i-'len h11+2 by AXIOMS:24; then 1+2-1<=i-'len h11+2-1 by REAL_1:49; then A944:1<k by A941,AXIOMS:22; A945:k in dom h2 by A22,A940,FINSEQ_3:27; then A946:h0.i=g2.(h2.k) by A937,FUNCT_1:23; A947: h2.k in rng h2 by A945,FUNCT_1:def 5; i in dom h0 by A744,A748,FINSEQ_3:27; then A948:h0/.i=h0.i by FINSEQ_4:def 4; g2.(h2.k) in rng g2 by A15,A16,A947,BORSUK_1:83,FUNCT_1:def 5; then h0.i in Upper_Arc(P) /\ Lower_Arc(P) by A13,A756,A924,A929,A946,A948,XBOOLE_0:def 3; then h0.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; then h0.i=W-min(P) or h0.i=E-max(P)by TARSKI:def 2; hence contradiction by A22,A28,A29,A30,A31,A65,A937,A942,A943, A944,A945,FUNCT_1:def 8; end; hence contradiction; case j+1>len h1; thus contradiction by A745,A897; end; hence contradiction; end; hence Segment(h0/.j,h0/.(j+1),P) misses Segment(h0/.i, h0/.(i+1),P) by A1,A753,A754,A898,A900,Th13; end; hence Segment(h0/.i,h0/.(i+1),P) misses Segment(h0/.j,h0/.(j+1),P); end; let i be Nat such that A949: 1 < i and A950: i+1 < len h0; A951: i<len h0 by A950,NAT_1:38; A952: LE h0/.i,h0/.(i+1),P by A550,A949,A950; A953: 1<i+1 by A949,NAT_1:38; A954: h0/.i<>h0/.(i+1) by A550,A949,A950; A955: i in dom h0 by A949,A951,FINSEQ_3:27; then h0/.i = h0.i by FINSEQ_4:def 4; then A956: h0/.i<>W-min P by A39,A61,A66,A949,A955,FUNCT_1:def 8; A957: i+1 in dom h0 by A950,A953,FINSEQ_3:27; A958: len h0-len h11 <= len (mid(h21,2,len h21 -'1)) by A40,XCMPLX_1:26; set k=len h0-'len h11+2-'1; 0<=len h0-'len h11 by NAT_1:18; then 0+2<=len h0-'len h11 +2 by AXIOMS:24; then A959: 2-'1<=len h0-'len h11 +2-'1 by JORDAN3:5; len h0-'len h11+2<=len h2-2+2 by A21,A47,A54,XCMPLX_1:26; then len h0-'len h11+2<=len h2 by XCMPLX_1:27; then (len h0-'len h11 +2-'1)<=len h21 by A23,JORDAN3:7; then A960: (len h0-'len h11 +2-'1) in dom h21 by A959,Lm2,FINSEQ_3:27; h0.len h0=mid(h21,2,len h21 -'1).(len h0 -len h11) by A21,A40,A48,FINSEQ_1:36; then A961: h0.len h0=h21.(len h0-'len h11 +2-'1) by A21,A43,A44,A53,A54,A958,JORDAN3:27; A962: h21.k=g2.(h2.k) by A22,A960,FUNCT_1:23; A963: h2.k in rng h2 by A22,A960,FUNCT_1:def 5; then A964: h0.len h0 in Lower_Arc(P) by A13,A15,A16,A961,A962,BORSUK_1:83, FUNCT_1:def 5; A965:LE h0/.(i+1),h0/.len h0,P proof per cases; suppose A966:i+1<=len h1; then A967: h0.(i+1)=h11.(i+1) by A21,A953,SCMFSA_7:9; i+1 in dom h1 by A953,A966,FINSEQ_3:27; then A968: h11.(i+1)=g1.(h1.(i+1)) by FUNCT_1:23; i+1 in dom h1 by A953,A966,FINSEQ_3:27; then A969: h1.(i+1) in rng h1 by FUNCT_1:def 5; A970:h0/.(i+1)=h0.(i+1) by A957,FINSEQ_4:def 4; g1.(h1.(i+1)) in rng g1 by A6,A9,A969,BORSUK_1:83, FUNCT_1:def 5; hence thesis by A4,A52,A121,A964,A967,A968,A970,JORDAN6:def 10; suppose A971:i+1>len h1; A972: 0<=len h0-'len h11 by A21,A49,A54,SQUARE_1:12; A973:len h0-len h11 <= len (mid(h21,2,len h21 -'1)) by A40,XCMPLX_1:26; 0+1<=len h0-'len h11+1 by A972,AXIOMS:24; then 0+1<=len h0-'len h11+1+1-1 by XCMPLX_1:26; then 0+1<=len h0-'len h11+(1+1)-1 by XCMPLX_1:1; then A974:len h0-'len h11+2-'1=len h0-'len h11+2-1 by JORDAN3 :1; len h0-'len h11+2<=len h2-2+2 by A21,A47,A54,XCMPLX_1:26; then len h0-'len h11+2<=len h2 by XCMPLX_1:27; then A975: (len h0-'len h11 +2-'1)<=len h21 by A23,JORDAN3:7; then A976:len h0-'len h11 +2-'1 in dom h21 by A959,Lm2,FINSEQ_3:27; A977: len h11+1<=i+1 by A21,A971,NAT_1:38; A978: i+1<len h11 + len (mid(h21,2,len h21 -'1)) by A950,FINSEQ_1: 35; i+1-len h11<len h11 + len (mid(h21,2,len h21 -'1)) - len h11 by A40,A950,REAL_1:54; then A979:i+1-len h11<len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; len h1+1<=i+1 by A971,NAT_1:38; then len h1+1-len h1<=i+1-len h1 by REAL_1:49; then A980: 1<=i+1-len h1 by XCMPLX_1:26; then A981: i+1-'len h11=i+1-len h11 by A21,JORDAN3:1; A982: h0.(i+1) = mid(h21,2,len h21 -'1).(i+1 -len h11) by A977,A978,FINSEQ_1:36 .= h21.(i+1-'len h11+2-'1) by A21,A43,A44,A979,A980,A981,JORDAN3:27; A983: (i+1)-len h11=(i+1)-'len h11 by A21,A971,SCMFSA_7:3; A984: (len h0-'len h11 +2-'1) in dom h21 by A959,A975,Lm2,FINSEQ_3: 27; h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11) by A21,A40,A48,FINSEQ_1:36; then A985:h0.len h0=h21.(len h0-'len h11 +2-'1) by A21,A43,A44,A53,A54,A973,JORDAN3:27; 0<=(i+1)-'len h11 by NAT_1:18; then 0+2<=(i+1)-'len h11 +2 by AXIOMS:24; then A986:2-'1<=((i+1)-'len h11 +2-'1) by JORDAN3:5; (i+1)-len h11<=len h11+(len h2-2)-len h11 by A21,A47,A950,REAL_1:49; then (i+1)-len h11<=(len h2-2) by XCMPLX_1:26; then (i+1)-'len h11+2<=len h2-2+2 by A983,AXIOMS:24; then (i+1)-'len h11+2<=len h2 by XCMPLX_1:27; then A987: (i+1)-'len h11 +2-'1 <= len h21 by A23,JORDAN3:7; A988:(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A986,Lm2,JORDAN3:1; set k=len h0-'len h11+2-'1; set j0=(i+1)-'len h11+2-'1; (i+1)-len h11<len h0-len h11 by A950,REAL_1:54; then (i+1)-'len h11+2<len h0-'len h11+2 by A54,A983,REAL_1:53 ; then A989:j0<k by A974,A988,REAL_1:54; A990:h21.k=g2.(h2.k) by A22,A976,FUNCT_1:23; A991: h2.k in rng h2 by A22,A984,FUNCT_1:def 5; then A992: 0<=h2.k by A16,BORSUK_1:83,TOPREAL5:1; A993: h2.k<=1 by A16,A991,BORSUK_1:83,TOPREAL5:1; A994:j0 in dom h2 by A22,A986,A987,Lm2,FINSEQ_3:27; then A995:h0.(i+1)=g2.(h2.j0) by A982,FUNCT_1:23; A996: h2.j0 in rng h2 by A994,FUNCT_1:def 5; then A997: 0<=h2.j0 by A16,BORSUK_1:83,TOPREAL5:1; A998: h2.j0<=1 by A16,A996,BORSUK_1:83,TOPREAL5:1; A999:h2.(j0)<h2.(k) by A16,A22,A984,A989,A994,GOBOARD1:def 1; A1000:h0/.(i+1)=h0.(i+1) by A957,FINSEQ_4:def 4; g2.(h2.j0) in rng g2 by A15,A16,A996,BORSUK_1:83,FUNCT_1:def 5; then A1001:h0.(i+1) in Lower_Arc(P) by A13,A982,A994,FUNCT_1: 23; h0.(len h0) in Lower_Arc(P) by A13,A15,A16,A961,A962,A963, BORSUK_1:83,FUNCT_1:def 5; then A1002: h0/.len h0 in Lower_Arc P by A51,FINSEQ_4:def 4; LE h0/.(i+1),h0/.len h0,Lower_Arc(P),E-max(P),W-min(P) by A11,A12,A13,A14,A52,A985,A990,A992,A993,A995,A997,A998,A999, A1000,Th19; hence thesis by A121,A1000,A1001,A1002,JORDAN6:def 10; end; now assume A1003:h0/.(i+1)=h0/.len h0; now per cases; case A1004:i+1<=len h1; i+1 in dom h0 by A950,A953,FINSEQ_3:27; then A1005:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; A1006:h0.(i+1)=h11.(i+1) by A21,A953,A1004,SCMFSA_7:9; A1007:i+1 in dom h1 by A953,A1004,FINSEQ_3:27; then A1008:h0.(i+1)=g1.(h1.(i+1)) by A1006,FUNCT_1:23; h1.(i+1) in rng h1 by A1007,FUNCT_1:def 5; then A1009:h0.(i+1) in Upper_Arc(P) by A4,A6,A9,A1008,BORSUK_1:83,FUNCT_1:def 5; A1010: h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11) by A21,A40,A48,FINSEQ_1:36; len h0-len h11<= len (mid(h21,2,len h21 -'1)) by A40,XCMPLX_1:26; then A1011:h0.len h0=h21.(len h0-'len h11 +2-'1) by A21,A43,A44,A53,A54,A1010,JORDAN3:27; 0<=len h0-'len h11 by NAT_1:18; then 0+2<=len h0-'len h11 +2 by AXIOMS:24; then A1012:2-'1<=(len h0-'len h11 +2-'1) by JORDAN3:5; len h0-'len h11+2<=len h2-2+2 by A21,A47,A54,XCMPLX_1:26; then len h0-'len h11+2<=len h2 by XCMPLX_1:27; then A1013: len h0-'len h11 +2-'1 <= len h21 by A23,JORDAN3:7; A1014:len h0-'len h11+2-'1=len h0-'len h11+2-1 by A1012,Lm2,JORDAN3:1; set k=len h0-'len h11+2-'1; len h0-'len h11+2<=len h2-2+2 by A21,A47,A54,XCMPLX_1:26; then A1015:len h0-'len h11+2<=len h2 by XCMPLX_1:27; len h0-'len h11+2-'1<len h0-'len h11+2-'1+1 by NAT_1:38; then A1016: len h0-'len h11+2-'1<len h0-'len h11+2 by A1014, XCMPLX_1:27; 1+2<=len h0-'len h11+2 by A55,AXIOMS:24; then 1+2-1<=len h0-'len h11+2-1 by REAL_1:49; then A1017:1<k by A1014,AXIOMS:22; A1018:k in dom h2 by A22,A1012,A1013,Lm2,FINSEQ_3:27; then A1019:h0.len h0=g2.(h2.k) by A1011,FUNCT_1:23; h2.k in rng h2 by A1018,FUNCT_1:def 5; then g2.(h2.k) in rng g2 by A15,A16,BORSUK_1:83,FUNCT_1:def 5 ; then h0.len h0 in Upper_Arc(P) /\ Lower_Arc(P) by A13,A52,A1003,A1005,A1009,A1019,XBOOLE_0:def 3; then A1020: h0.len h0 in {W-min(P),E-max(P)} by A1,JORDAN6:def 9; A1021: h0.len h0 <> W-min P by A22,A29,A31,A65,A1011,A1015,A1016,A1018,FUNCT_1:def 8; h0.len h0 <> E-max P by A22,A28,A30,A65,A1011,A1017,A1018,FUNCT_1:def 8; hence contradiction by A1020,A1021,TARSKI:def 2; case A1022:i+1>len h1; then A1023:len h1 +1<=i+1 by NAT_1:38; A1024: i+1 <= len h11 + len mid(h21,2,len h21 -'1) by A950,FINSEQ_1:35; A1025:h0.(i+1)=(mid(h21,2,len h21 -'1)).((i+1) -len h11) by A21,A40,A950,A1023,FINSEQ_1:36; A1026:(i+1)-len h11=(i+1)-'len h11 by A21,A1022,SCMFSA_7:3; i+1-len h11 <=len h11 + len mid(h21,2,len h21 -'1)-len h11 by A1024,REAL_1:49; then A1027:(i+1)-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26; len h1 +1-len h1<=(i+1)-len h1 by A1023,REAL_1:49; then 1<=(i+1)-len h11 by A21,XCMPLX_1:26; then A1028:h0.(i+1)=h21.((i+1)-'len h11 +2-'1) by A43,A44,A1025,A1026,A1027,JORDAN3:27; 0<=(i+1)-'len h11 by NAT_1:18; then 0+2<=(i+1)-'len h11 +2 by AXIOMS:24; then A1029:2-'1<=((i+1)-'len h11 +2-'1) by JORDAN3:5; (i+1)-len h11<=len h1+(len h2-2)-len h11 by A47,A950,REAL_1:49; then (i+1)-len h11<=(len h2-2) by A21,XCMPLX_1:26; then (i+1)-'len h11+2<=len h2-2+2 by A1026,AXIOMS:24; then (i+1)-'len h11+2<=len h2 by XCMPLX_1:27; then A1030: (i+1)-'len h11 +2-'1 <= len h21 by A23,JORDAN3:7; A1031:(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A1029,Lm2,JORDAN3:1; set j0=(i+1)-'len h11+2-'1; len h11+1-len h11<=(i+1)-len h11 by A21,A1023,REAL_1:49; then 1<=(i+1)-len h11 by XCMPLX_1:26; then A1032:(i+1)-'len h11=(i+1)-len h11 by JORDAN3:1; A1033:j0 in dom h2 by A22,A1029,A1030,Lm2,FINSEQ_3:27; 1<=i+1 by A949,NAT_1:38; then i+1 in dom h0 by A950,FINSEQ_3:27; then A1034:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4; A1035: h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11) by A21,A40,A48,FINSEQ_1:36; len h0-len h11<= len (mid(h21,2,len h21 -'1)) by A40,XCMPLX_1:26; then A1036:h0.len h0=h21.(len h0-'len h11 +2-'1) by A43,A44,A54,A55,A1035,JORDAN3:27; 0<=len h0-'len h11 by NAT_1:18; then 0+2<=len h0-'len h11 +2 by AXIOMS:24; then A1037:2-'1<=(len h0-'len h11 +2-'1) by JORDAN3:5; len h0-'len h11+2<=len h2-2+2 by A21,A47,A54,XCMPLX_1:26; then len h0-'len h11+2<=len h2 by XCMPLX_1:27; then A1038: len h0-'len h11 +2-'1 <= len h21 by A23,JORDAN3:7; A1039:len h0-'len h11+2-'1=len h0-'len h11+2-1 by A1037,Lm2,JORDAN3:1; set k=len h0-'len h11+2-'1; len h0-'len h11=len h0-len h11 by A21,A53,JORDAN3:1; then i+1-'len h11<len h0-'len h11 by A950,A1032,REAL_1:54; then i+1-'len h11+2<len h0-'len h11+2 by REAL_1:53; then A1040: (i+1)-'len h11+2-'1<len h0-'len h11+2 -'1 by A1031,A1039,REAL_1:54; k in dom h2 by A22,A1037,A1038,Lm2,FINSEQ_3:27; hence contradiction by A22,A52,A65,A1003,A1028,A1033,A1034,A1036, A1040,FUNCT_1:def 8; end; hence contradiction; end; hence Segment(h0/.len h0,h0/.1,P) misses Segment(h0/.i,h0/.(i+1),P) by A1,A39,A62,A952,A954,A956,A965,Th14; end;