:: Jordan Curve Theorem :: by Artur Korni{\l}owicz :: :: Received September 15, 2005 :: Copyright (c) 2005-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, TOPREAL2, RELAT_1, RCOMP_1, JORDAN21, TARSKI, XBOOLE_0, RELAT_2, METRIC_1, XXREAL_0, CARD_1, ARYTM_3, SUPINF_2, ARYTM_1, MCART_1, SPPOL_1, RLTOPSP1, PSCOMP_1, JORDAN6, JORDAN2C, CONVEX1, TOPREAL1, STRUCT_0, TOPMETR, VALUED_1, TREAL_1, ZFMISC_1, REAL_1, FUNCOP_1, ORDINAL2, COMPLEX1, BROUWER, TOPREALB, XCMPLX_0, TOPS_1, PCOMPS_1, XXREAL_2, FUNCT_1, TOPS_2, FUNCT_2, GRAPH_1, BORSUK_2, BORSUK_1, XXREAL_1, JGRAPH_6, JORDAN5C, JORDAN3, SQUARE_1, PARTFUN3, PARTFUN1, TOPREALA, SETFAM_1, PROB_1, ABIAN, CONNSP_1, CONNSP_2, TOPREAL4, FUNCT_4, TOPGRP_1, JORDAN24, CONNSP_3, JORDAN1, JORDAN, MEASURE5, SEQ_4, NAT_1, FUNCT_7; notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, SQUARE_1, MCART_1, RELAT_1, VALUED_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, FUNCT_4, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, COMPLEX1, REAL_1, RCOMP_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TOPS_2, COMPTS_1, TREAL_1, CONNSP_1, CONNSP_2, CONNSP_3, METRIC_1, TBSP_1, RLVECT_1, PCOMPS_1, RLTOPSP1, EUCLID, BORSUK_2, TOPREAL1, TOPREAL2, TOPMETR, SPPOL_1, JORDAN1, JORDAN2C, JORDAN5C, TOPREAL4, JORDAN6, JGRAPH_6, TOPREAL6, TOPREAL9, BORSUK_6, TOPREALA, JORDAN21, TOPGRP_1, JORDAN24, ABIAN, PARTFUN3, TOPREALB, BROUWER, PSCOMP_1; constructors FUNCT_4, SQUARE_1, COMPLEX1, ABIAN, TOPS_1, CONNSP_1, COMPTS_1, TBSP_1, TSEP_1, TOPREAL1, TREAL_1, TOPREAL4, SPPOL_1, JORDAN1, SPPOL_2, CONNSP_3, WAYBEL_3, JORDAN5C, JORDAN6, TOPGRP_1, JORDAN2C, TOPREAL6, JORDAN21, JGRAPH_6, TOPREAL9, TOPREALA, PARTFUN3, BROUWER, JORDAN24, BORSUK_6, SEQ_4, FUNCSDOM, CONVEX1, BINOP_2, PSCOMP_1, XTUPLE_0, REAL_1; registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, METRIC_1, BORSUK_1, TEX_2, TEX_4, EUCLID, TOPMETR, TOPREAL1, TOPREAL2, SPPOL_1, JORDAN1, SPPOL_2, PSCOMP_1, BORSUK_2, WAYBEL_2, WAYBEL_3, JORDAN5A, JORDAN6, TOPGRP_1, YELLOW13, JORDAN2C, TOPREAL6, JORDAN21, TOPREAL9, TOPREALA, TOPREALB, RCOMP_3, PARTFUN3, TOPALG_5, BROUWER, JGRAPH_8, VALUED_0, XXREAL_2, RELAT_1, MEASURE6, PARTFUN4, VALUED_1, XTUPLE_0, ORDINAL1, CARD_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; definitions TARSKI, XBOOLE_0, BORSUK_2, JORDAN1, SPPOL_1, JORDAN2C, JORDAN21, JORDAN24, TOPREAL2, CONNSP_1, BORSUK_1, PSCOMP_1, ABIAN, XXREAL_0; equalities JORDAN2C, JORDAN21, PSCOMP_1, SQUARE_1, JGRAPH_6, TOPS_1, SUBSET_1, TOPREALA, STRUCT_0, RELAT_1, ALGSTR_0, RLTOPSP1; expansions TARSKI, XBOOLE_0, BORSUK_2, JORDAN1, SPPOL_1, JORDAN2C, JORDAN24, CONNSP_1, ABIAN; theorems JORDAN6, PRE_TOPC, XBOOLE_0, EUCLID, TARSKI, SQUARE_1, CONNSP_1, JORDAN2C, JGRAPH_6, XREAL_1, JORDAN1K, TOPREAL6, BORSUK_2, JORDAN21, TOPREAL1, TOPREAL3, SPPOL_1, SUBSET_1, TOPMETR, TOPREAL9, TOPS_1, SPRECT_3, TOPRNS_1, TOPS_2, NAT_1, JORDAN1, TOPREALA, BORSUK_1, FUNCT_2, RELAT_1, GOBOARD7, FUNCT_1, BORSUK_6, XBOOLE_1, ZFMISC_1, CONNSP_3, TOPALG_2, GOBOARD9, SPPOL_2, PSCOMP_1, TOPREAL4, TSEP_1, TOPALG_3, JGRAPH_8, COMPTS_1, SEQ_4, FUNCOP_1, WEIERSTR, JORDAN5C, JORDAN16, XREAL_0, XCMPLX_1, SPRECT_1, JORDAN24, TOPGRP_1, TOPREAL2, RCOMP_1, BORSUK_4, BROUWER, ENUMSET1, METRIC_1, PCOMPS_1, TOPREALB, ABSVALUE, MCART_1, BORSUK_5, METRIC_6, COMPLEX1, JGRAPH_2, SEQ_2, TIETZE, CONNSP_2, GRCAT_1, FUNCT_4, TREAL_1, JGRAPH_1, PARTFUN3, RFUNCT_1, YELLOW12, XCMPLX_0, FUNCT_3, JORDAN5B, TOPALG_5, GOBOARD6, XXREAL_0, VALUED_1, XXREAL_1, RLTOPSP1, ORDINAL1, JORDAN5A, RLVECT_1; schemes FUNCT_2; begin :: Preliminaries :: I would like to thank Professor Yatsuka Nakamura :: for including me to the team working on the formalization :: of the Jordan Curve Theorem. Especially, I am very grateful :: to Professor Nakamura for inviting me to Shinshu University, Nagano :: to work on the project together. :: I am also thankful to Professor Andrzej Trybulec for his :: continual help and fruitful discussions during the formalization. reserve a, b, c, d, r, s for Real, n for Element of NAT, p, p1, p2 for Point of TOP-REAL 2, x, y for Point of TOP-REAL n, C for Simple_closed_curve, A, B, P for Subset of TOP-REAL 2, U, V for Subset of (TOP-REAL 2)|C`, D for compact with_the_max_arc Subset of TOP-REAL 2; set T2 = TOP-REAL 2; Lm1: for A, B, C, Z being set st A c= Z & B c= Z & C c= Z holds A \/ B \/ C c= Z proof let A, B, C, Z be set; assume that A1: A c= Z and A2: B c= Z; A \/ B c= Z by A1,A2,XBOOLE_1:8; hence thesis by XBOOLE_1:8; end; Lm2: for A, B, C, D, Z being set st A c= Z & B c= Z & C c= Z & D c= Z holds A \/ B \/ C \/ D c= Z proof let A, B, C, D, Z be set; assume that A1: A c= Z and A2: B c= Z and A3: C c= Z; A \/ B \/ C c= Z by A1,A2,A3,Lm1; hence thesis by XBOOLE_1:8; end; Lm3: for A, B, C, D, Z being set st A misses Z & B misses Z & C misses Z & D misses Z holds A \/ B \/ C \/ D misses Z proof let A, B, C, D, Z be set; assume that A1: A misses Z and A2: B misses Z and A3: C misses Z; A \/ B \/ C misses Z by A1,A2,A3,XBOOLE_1:114; hence thesis by XBOOLE_1:70; end; registration let M be symmetric triangle Reflexive MetrStruct, x, y be Point of M; cluster dist(x,y) -> non negative; coherence by METRIC_1:5; end; registration let n be Element of NAT, x, y be Point of TOP-REAL n; cluster dist(x,y) -> non negative; coherence proof ex p, q being Point of Euclid n st p = x & q = y & dist(x,y) = dist(p,q) by TOPREAL6:def 1; hence 0 <= dist(x,y); end; end; theorem Th1: for p1, p2 being Point of TOP-REAL n st p1 <> p2 holds 1/2*(p1+p2) <> p1 proof let p1, p2 be Point of TOP-REAL n; set r = 1/2; assume that A1: p1 <> p2 and A2: r*(p1+p2) = p1; r*(p1+p2) = r*p1+r*p2 by RLVECT_1:def 5; then 0.TOP-REAL n = p1-(r*p1+r*p2) by A2,RLVECT_1:5 .= p1-r*p1-r*p2 by RLVECT_1:27 .= 1 * p1-r*p1-r*p2 by RLVECT_1:def 8 .= (1-r)*p1-r*p2 by RLVECT_1:35 .= r*(p1-p2) by RLVECT_1:34; then p1-p2 = 0.TOP-REAL n by RLVECT_1:11; hence thesis by A1,RLVECT_1:21; end; theorem Th2: p1`2 < p2`2 implies p1`2 < (1/2*(p1+p2))`2 proof assume A1: p1`2 < p2`2; (1/2*(p1+p2))`2 = 1/2*((p1+p2)`2) by TOPREAL3:4 .= 1/2*(p1`2+p2`2) by TOPREAL3:2 .= (p1`2+p2`2)/2; hence thesis by A1,XREAL_1:226; end; theorem Th3: p1`2 < p2`2 implies (1/2*(p1+p2))`2 < p2`2 proof assume A1: p1`2 < p2`2; (1/2*(p1+p2))`2 = 1/2*((p1+p2)`2) by TOPREAL3:4 .= 1/2*(p1`2+p2`2) by TOPREAL3:2 .= (p1`2+p2`2)/2; hence thesis by A1,XREAL_1:226; end; theorem Th4: for A being vertical Subset of TOP-REAL 2 holds A /\ B is vertical proof let A be vertical Subset of TOP-REAL 2; let p, q be Point of T2; assume that A1: p in A /\ B and A2: q in A /\ B; A3: p in A by A1,XBOOLE_0:def 4; q in A by A2,XBOOLE_0:def 4; hence thesis by A3,SPPOL_1:def 3; end; theorem for A being horizontal Subset of TOP-REAL 2 holds A /\ B is horizontal proof let A be horizontal Subset of TOP-REAL 2; let p, q be Point of T2; assume that A1: p in A /\ B and A2: q in A /\ B; A3: p in A by A1,XBOOLE_0:def 4; q in A by A2,XBOOLE_0:def 4; hence thesis by A3,SPPOL_1:def 2; end; theorem p in LSeg(p1,p2) & LSeg(p1,p2) is vertical implies LSeg(p,p2) is vertical proof assume A1: p in LSeg(p1,p2); assume A2: LSeg(p1,p2) is vertical; then A3: p1`1 = p2`1 by SPPOL_1:16; p1 in LSeg(p1,p2) by RLTOPSP1:68; then p`1 = p1`1 by A1,A2; hence thesis by A3,SPPOL_1:16; end; theorem p in LSeg(p1,p2) & LSeg(p1,p2) is horizontal implies LSeg(p,p2) is horizontal proof assume A1: p in LSeg(p1,p2); assume A2: LSeg(p1,p2) is horizontal; then A3: p1`2 = p2`2 by SPPOL_1:15; p1 in LSeg(p1,p2) by RLTOPSP1:68; then p`2 = p1`2 by A1,A2; hence thesis by A3,SPPOL_1:15; end; registration :: LSeg(NW-corner C,NE-corner C) is horizontal; ::SPRECT_3:29 let P be Subset of TOP-REAL 2; cluster LSeg(SW-corner P,SE-corner P) -> horizontal; coherence proof (SW-corner P)`2 = S-bound P by EUCLID:52 .= (SE-corner P)`2 by EUCLID:52; hence thesis by SPPOL_1:15; end; cluster LSeg(NW-corner P,SW-corner P) -> vertical; coherence proof (NW-corner P)`1 = W-bound P by EUCLID:52 .= (SW-corner P)`1 by EUCLID:52; hence thesis by SPPOL_1:16; end; cluster LSeg(NE-corner P,SE-corner P) -> vertical; coherence proof (NE-corner P)`1 = E-bound P by EUCLID:52 .= (SE-corner P)`1 by EUCLID:52; hence thesis by SPPOL_1:16; end; end; registration let P be Subset of TOP-REAL 2; cluster LSeg(SE-corner P,SW-corner P) -> horizontal; coherence; cluster LSeg(SW-corner P,NW-corner P) -> vertical; coherence; cluster LSeg(SE-corner P,NE-corner P) -> vertical; coherence; end; registration cluster vertical non empty compact -> with_the_max_arc for Subset of TOP-REAL 2; coherence proof let A be Subset of TOP-REAL 2; assume A1: A is vertical non empty compact; then A2: W-bound A = E-bound A by SPRECT_1:15; A3: E-min A in A by A1,SPRECT_1:14; (E-min A)`1 = E-bound A by EUCLID:52; then E-min A in Vertical_Line((W-bound A+E-bound A)/2) by A2,JORDAN6:31; hence A meets Vertical_Line((W-bound A+E-bound A)/2) by A3,XBOOLE_0:3; end; end; theorem Th8: p1`1 <= r & r <= p2`1 implies LSeg(p1,p2) meets Vertical_Line(r) proof assume that A1: p1`1 <= r and A2: r <= p2`1; set a = p1`1, b = p2`1; set l = (r-a) / (b-a); set k = (1-l)*p1+l*p2; A3: a-a <= r-a by A1,XREAL_1:9; A4: r-a <= b-a by A2,XREAL_1:9; then l <= 1 by A3,XREAL_1:183; then A5: k in LSeg(p1,p2) by A3,A4; per cases; suppose a <> b; then A6: b-a <> 0; k`1 = (1-l)*a+l*b by TOPREAL9:41 .= a+l*(b-a) .= a+(r-a) by A6,XCMPLX_1:87; then k in Vertical_Line(r) by JORDAN6:31; hence thesis by A5,XBOOLE_0:3; end; suppose A7: a = b; A8: p1 in LSeg(p1,p2) by RLTOPSP1:68; a = r by A1,A2,A7,XXREAL_0:1; then p1 in Vertical_Line(r) by JORDAN6:31; hence thesis by A8,XBOOLE_0:3; end; end; theorem p1`2 <= r & r <= p2`2 implies LSeg(p1,p2) meets Horizontal_Line(r) proof assume that A1: p1`2 <= r and A2: r <= p2`2; set a = p1`2, b = p2`2; set l = (r-a) / (b-a); set k = (1-l)*p1+l*p2; A3: a-a <= r-a by A1,XREAL_1:9; A4: r-a <= b-a by A2,XREAL_1:9; then l <= 1 by A3,XREAL_1:183; then A5: k in LSeg(p1,p2) by A3,A4; per cases; suppose a <> b; then A6: b-a <> 0; k`2 = (1-l)*a+l*b by TOPREAL9:42 .= a+l*(b-a) .= a+(r-a) by A6,XCMPLX_1:87; then k in Horizontal_Line(r) by JORDAN6:32; hence thesis by A5,XBOOLE_0:3; end; suppose A7: a = b; A8: p1 in LSeg(p1,p2) by RLTOPSP1:68; a = r by A1,A2,A7,XXREAL_0:1; then p1 in Horizontal_Line(r) by JORDAN6:32; hence thesis by A8,XBOOLE_0:3; end; end; registration let n; cluster empty -> bounded for Subset of TOP-REAL n; coherence; cluster non bounded -> non empty for Subset of TOP-REAL n; coherence; end; registration let n be non zero Nat; cluster open closed non bounded convex for Subset of TOP-REAL n; existence proof take [#]TOP-REAL n; reconsider n as Element of NAT by ORDINAL1:def 12; n >= 1 by NAT_1:14; then [#]TOP-REAL n is not bounded by JORDAN2C:35; hence thesis; end; end; theorem Th10: for C being compact Subset of TOP-REAL 2 holds north_halfline UMP C \ {UMP C} misses C proof let C be compact Subset of TOP-REAL 2; set p = UMP C; set L = north_halfline p; set w = (W-bound C + E-bound C) / 2; assume L \ {p} meets C; then consider x being object such that A1: x in L \ {p} and A2: x in C by XBOOLE_0:3; A3: x in L by A1,ZFMISC_1:56; A4: x <> p by A1,ZFMISC_1:56; reconsider x as Point of T2 by A1; A5: x`1 = p`1 by A3,TOPREAL1:def 10; A6: x`2 >= p`2 by A3,TOPREAL1:def 10; x`2 <> p`2 by A4,A5,TOPREAL3:6; then A7: x`2 > p`2 by A6,XXREAL_0:1; x`1 = w by A5,EUCLID:52; then x in Vertical_Line w by JORDAN6:31; then x in C /\ Vertical_Line w by A2,XBOOLE_0:def 4; hence thesis by A7,JORDAN21:28; end; theorem Th11: for C being compact Subset of TOP-REAL 2 holds south_halfline LMP C \ {LMP C} misses C proof let C be compact Subset of TOP-REAL 2; set p = LMP C; set L = south_halfline p; set w = (W-bound C + E-bound C) / 2; assume L \ {p} meets C; then consider x being object such that A1: x in L \ {p} and A2: x in C by XBOOLE_0:3; A3: x in L by A1,ZFMISC_1:56; A4: x <> p by A1,ZFMISC_1:56; reconsider x as Point of T2 by A1; A5: x`1 = p`1 by A3,TOPREAL1:def 12; A6: x`2 <= p`2 by A3,TOPREAL1:def 12; x`2 <> p`2 by A4,A5,TOPREAL3:6; then A7: x`2 < p`2 by A6,XXREAL_0:1; x`1 = w by A5,EUCLID:52; then x in Vertical_Line w by JORDAN6:31; then x in C /\ Vertical_Line w by A2,XBOOLE_0:def 4; hence thesis by A7,JORDAN21:29; end; theorem Th12: for C being compact Subset of TOP-REAL 2 holds north_halfline UMP C \ {UMP C} c= UBD C proof let C be compact Subset of TOP-REAL 2; set A = north_halfline UMP C \ {UMP C}; reconsider A as non bounded Subset of T2 by JORDAN2C:122,TOPREAL6:90; A is convex by JORDAN21:6; hence thesis by Th10,JORDAN2C:125; end; theorem Th13: for C being compact Subset of TOP-REAL 2 holds south_halfline LMP C \ {LMP C} c= UBD C proof let C be compact Subset of TOP-REAL 2; set A = south_halfline LMP C \ {LMP C}; reconsider A as non bounded Subset of T2 by JORDAN2C:123,TOPREAL6:90; A is convex by JORDAN21:7; hence thesis by Th11,JORDAN2C:125; end; theorem Th14: A is_inside_component_of B implies UBD B misses A proof assume A is_inside_component_of B; then A c= BDD B by JORDAN2C:22; hence thesis by JORDAN2C:24,XBOOLE_1:63; end; theorem A is_outside_component_of B implies BDD B misses A proof assume A1: A is_outside_component_of B; BDD B misses UBD B by JORDAN2C:24; hence thesis by A1,JORDAN2C:23,XBOOLE_1:63; end; Lm4: p in C implies {p} misses U proof assume A1: p in C; A2: U is Subset of T2 by PRE_TOPC:11; the carrier of T2|C` = C` by PRE_TOPC:8; then U misses C by A2,SUBSET_1:23; then not p in U by A1,XBOOLE_0:3; hence thesis by ZFMISC_1:50; end; set C0 = Closed-Interval-TSpace(0,1); set C1 = Closed-Interval-TSpace(-1,1); set l0 = (#)(-1,1); set l1 = (-1,1)(#); set h1 = L[01](l0,l1); Lm5: the carrier of [:T2,T2:] = [:the carrier of T2, the carrier of T2:] by BORSUK_1:def 2; Lm6: now let T be non empty TopSpace; let a be Element of REAL; set c = the carrier of T; set f = c --> a; thus f is continuous proof A1: dom f = c by FUNCT_2:def 1; A2: rng f = {a} by FUNCOP_1:8; let Y be Subset of REAL; assume Y is closed; per cases; suppose a in Y; then A3: rng f c= Y by A2,ZFMISC_1:31; f"Y = f"(rng f /\ Y) by RELAT_1:133 .= f"rng f by A3,XBOOLE_1:28 .= [#]T by A1,RELAT_1:134; hence thesis; end; suppose not a in Y; then A4: rng f misses Y by A2,ZFMISC_1:50; f"Y = f"(rng f /\ Y) by RELAT_1:133 .= f"{} by A4 .= {}T; hence thesis; end; end; end; theorem Th16: for n being Nat for r being positive Real for a being Point of TOP-REAL n holds a in Ball(a,r) proof let n be Nat; let r be positive Real; let a be Point of TOP-REAL n; |. a-a .| = 0 by TOPRNS_1:28; hence thesis by TOPREAL9:7; end; theorem Th17: for r being non negative Real for p being Point of TOP-REAL n holds p is Point of Tdisk(p,r) proof let r be non negative Real; let p be Point of TOP-REAL n; A1: the carrier of Tdisk(p,r) = cl_Ball(p,r) by BROUWER:3; |. p-p .| = 0 by TOPRNS_1:28; hence thesis by A1,TOPREAL9:8; end; registration let r be positive Real; let n be non zero Element of NAT; let p, q be Point of TOP-REAL n; cluster cl_Ball(p,r) \ {q} -> non empty; coherence proof A1: the carrier of Tcircle(p,r) = Sphere(p,r) by TOPREALB:9; A2: the carrier of Tdisk(p,r) = cl_Ball(p,r) by BROUWER:3; A3: Sphere(p,r) c= cl_Ball(p,r) by TOPREAL9:17; set a = the Point of Tcircle(p,r); A4: a in Sphere(p,r) by A1; per cases; suppose A5: a = q; A6: p is Point of Tdisk(p,r) by Th17; |. p-p .| <> r by TOPRNS_1:28; then p <> q by A1,A5,TOPREAL9:9; hence thesis by A2,A6,ZFMISC_1:56; end; suppose a <> q; hence thesis by A3,A4,ZFMISC_1:56; end; end; end; theorem Th18: r <= s implies Ball(x,r) c= Ball(x,s) proof reconsider xe = x as Point of Euclid n by TOPREAL3:8; A1: Ball(x,r) = Ball(xe,r) by TOPREAL9:13; Ball(x,s) = Ball(xe,s) by TOPREAL9:13; hence thesis by A1,PCOMPS_1:1; end; theorem Th19: cl_Ball(x,r) \ Ball(x,r) = Sphere(x,r) proof thus cl_Ball(x,r) \ Ball(x,r) c= Sphere(x,r) proof let a be object; assume A1: a in cl_Ball(x,r) \ Ball(x,r); then reconsider a as Point of TOP-REAL n; A2: a in cl_Ball(x,r) by A1,XBOOLE_0:def 5; A3: not a in Ball(x,r) by A1,XBOOLE_0:def 5; A4: |. a-x .| <= r by A2,TOPREAL9:8; |. a-x .| >= r by A3,TOPREAL9:7; then |. a-x .| = r by A4,XXREAL_0:1; hence thesis by TOPREAL9:9; end; let a be object; assume A5: a in Sphere(x,r); then reconsider a as Point of TOP-REAL n; A6: |. a-x .| = r by A5,TOPREAL9:9; then A7: a in cl_Ball(x,r) by TOPREAL9:8; not a in Ball(x,r) by A6,TOPREAL9:7; hence thesis by A7,XBOOLE_0:def 5; end; theorem Th20: y in Sphere(x,r) implies LSeg(x,y) \ {x,y} c= Ball(x,r) proof assume A1: y in Sphere(x,r); per cases; suppose A2: r = 0; reconsider xe = x as Point of Euclid n by TOPREAL3:8; Sphere(x,r) = Sphere(xe,r) by TOPREAL9:15; then Sphere(x,r) = {x} by A2,TOPREAL6:54; then A3: x = y by A1,TARSKI:def 1; A4: LSeg(x,x) = {x} by RLTOPSP1:70; A5: {x,x} = {x} by ENUMSET1:29; {x} \ {x} = {} by XBOOLE_1:37; hence thesis by A3,A4,A5; end; suppose A6: r <> 0; let k be object; assume A7: k in LSeg(x,y) \ {x,y}; then k in LSeg(x,y) by XBOOLE_0:def 5; then consider l being Real such that A8: k = (1-l)*x + l*y and A9: 0 <= l and A10: l <= 1; reconsider k as Point of TOP-REAL n by A8; not k in {x,y} by A7,XBOOLE_0:def 5; then k <> y by TARSKI:def 2; then l <> 1 by A8,TOPREAL9:4; then A11: l < 1 by A10,XXREAL_0:1; k-x = (1-l)*x - x + l*y by A8,RLVECT_1:def 3 .= 1 * x - l*x - x + l*y by RLVECT_1:35 .= x - l*x - x + l*y by RLVECT_1:def 8 .= x +- l*x +- x + l*y .= x +- x +- l*x + l*y by RLVECT_1:def 3 .= x - x - l*x + l*y .= 0.TOP-REAL n - l*x + l*y by RLVECT_1:5 .= l*y - l*x by RLVECT_1:4 .= l*(y-x) by RLVECT_1:34; then A12: |. k-x .| = |.l.| * |. y-x .| by TOPRNS_1:7 .= l*|. y-x .| by A9,ABSVALUE:def 1 .= l*r by A1,TOPREAL9:9; 0 <= r by A1; then l*r < 1 * r by A6,A11,XREAL_1:68; hence thesis by A12,TOPREAL9:7; end; end; theorem Th21: r < s implies cl_Ball(x,r) c= Ball(x,s) proof assume A1: r < s; let a be object; assume A2: a in cl_Ball(x,r); then reconsider a as Point of TOP-REAL n; |. a-x .| <= r by A2,TOPREAL9:8; then |. a-x .| < s by A1,XXREAL_0:2; hence thesis by TOPREAL9:7; end; theorem Th22: r < s implies Sphere(x,r) c= Ball(x,s) proof assume r < s; then A1: cl_Ball(x,r) c= Ball(x,s) by Th21; Sphere(x,r) c= cl_Ball(x,r) by TOPREAL9:17; hence thesis by A1; end; theorem Th23: for r being non zero Real holds Cl Ball(x,r) = cl_Ball(x,r) proof let r be non zero Real; thus Cl Ball(x,r) c= cl_Ball(x,r) by TOPREAL9:16,TOPS_1:5; per cases; suppose Ball(x,r) is empty; then r < 0; hence thesis; end; suppose A1: Ball(x,r) is non empty; let a be object; assume A2: a in cl_Ball(x,r); then reconsider a as Point of TOP-REAL n; reconsider ae = a as Point of Euclid n by TOPREAL3:8; A3: 0 < r by A1; for s being Real st 0 < s & s < r holds Ball(ae,s) meets Ball(x,r) proof let s be Real such that A4: 0 < s and A5: s < r; now A6: Ball(x,r) \/ Sphere(x,r) = cl_Ball(x,r) by TOPREAL9:18; per cases by A2,A6,XBOOLE_0:def 3; suppose A7: a in Ball(x,r); |.a-a.| = 0 by TOPRNS_1:28; then a in Ball(a,s) by A4,TOPREAL9:7; hence Ball(a,s) meets Ball(x,r) by A7,XBOOLE_0:3; end; suppose A8: a in Sphere(x,r); then A9: |. a-x .| = r by TOPREAL9:9; |. x-x .| = 0 by TOPRNS_1:28; then A10: x in Ball(x,r) by A3,TOPREAL9:7; set z = s/(2*r); set q = (1-z)*a+z*x; 1 * r < 2*r by A3,XREAL_1:68; then s < 2*r by A5,XXREAL_0:2; then A11: z < 1 by A4,XREAL_1:189; 0 < 2*r by A3,XREAL_1:129; then A12: 0 < z by A4,XREAL_1:139; A13: q in LSeg(a,x) by A3,A4,A11; Ball(x,r) misses Sphere(x,r) by TOPREAL9:19; then A14: a <> x by A8,A10,XBOOLE_0:3; then A15: q <> a by A12,TOPREAL9:4; q <> x by A11,A14,TOPREAL9:4; then not q in {a,x} by A15,TARSKI:def 2; then A16: q in LSeg(a,x) \ {a,x} by A13,XBOOLE_0:def 5; A17: LSeg(a,x) \ {a,x} c= Ball(x,r) by A8,Th20; q-a = (1-z)*a - a + z*x by RLVECT_1:def 3 .= 1 * a - z*a - a + z*x by RLVECT_1:35 .= a - z*a - a + z*x by RLVECT_1:def 8 .= a +- z*a +- a + z*x .= a +- a +- z*a + z*x by RLVECT_1:def 3 .= a - a - z*a + z*x .= 0.TOP-REAL n - z*a + z*x by RLVECT_1:5 .= z*x - z*a by RLVECT_1:4 .= z*(x-a) by RLVECT_1:34; then |.q-a.| = |.z.| * |.x-a.| by TOPRNS_1:7 .= z*|.x-a.| by A3,A4,ABSVALUE:def 1 .= z*|. a-x .| by TOPRNS_1:27 .= s/2 by A9,XCMPLX_1:92; then A18: q in Sphere(a,s/2) by TOPREAL9:9; s/2 < s/1 by A4,XREAL_1:76; then Sphere(a,s/2) c= Ball(a,s) by Th22; hence Ball(a,s) meets Ball(x,r) by A16,A17,A18,XBOOLE_0:3; end; end; hence thesis by TOPREAL9:13; end; hence thesis by A3,GOBOARD6:93; end; end; theorem Th24: for r being non zero Real holds Fr Ball(x,r) = Sphere(x,r) proof let r be non zero Real; set P = Ball(x,r); thus Fr P = Cl P \ P by TOPS_1:42 .= cl_Ball(x,r) \ P by Th23 .= Sphere(x,r) by Th19; end; registration let n be non zero Element of NAT; cluster bounded -> proper for Subset of TOP-REAL n; coherence proof [#]TOP-REAL n is not bounded by JORDAN2C:35,NAT_1:14; hence thesis by SUBSET_1:def 6; end; end; registration let n; cluster non empty closed convex bounded for Subset of TOP-REAL n; existence proof take cl_Ball(0.TOP-REAL n,1); thus thesis; end; cluster non empty open convex bounded for Subset of TOP-REAL n; existence proof take Ball(0.TOP-REAL n,1); thus thesis; end; end; registration let n be Element of NAT; let A be bounded Subset of TOP-REAL n; cluster Cl A -> bounded; coherence by TOPREAL6:63; end; registration let n be Element of NAT; let A be bounded Subset of TOP-REAL n; cluster Fr A -> bounded; coherence by TOPREAL6:89; end; theorem Th25: for A being closed Subset of TOP-REAL n, p being Point of TOP-REAL n st not p in A ex r being positive Real st Ball(p,r) misses A proof let A be closed Subset of TOP-REAL n, p be Point of TOP-REAL n; assume not p in A; then A1: p in A` by SUBSET_1:29; reconsider e = p as Point of Euclid n by TOPREAL3:8; A2: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider AA = A` as Subset of TopSpaceMetr Euclid n; AA is open by A2,PRE_TOPC:30; then consider r being Real such that A3: r > 0 and A4: Ball(e,r) c= A` by A1,TOPMETR:15; reconsider r as positive Real by A3; take r; Ball(p,r) = Ball(e,r) by TOPREAL9:13; hence thesis by A4,SUBSET_1:23; end; theorem Th26: for A being bounded Subset of TOP-REAL n, a being Point of TOP-REAL n ex r being positive Real st A c= Ball(a,r) proof let A be bounded Subset of TOP-REAL n; let a be Point of TOP-REAL n; reconsider C = A as bounded Subset of Euclid n by JORDAN2C:11; consider r being Real, x being Element of Euclid n such that A1: 0 < r and A2: C c= Ball(x,r) by METRIC_6:def 3; reconsider r as positive Real by A1; reconsider x1 = x as Point of TOP-REAL n by TOPREAL3:8; take s = r+|.x1-a.|; let p be object; assume A3: p in A; then reconsider p1 = p as Point of TOP-REAL n; p = p1; then reconsider p as Point of Euclid n by TOPREAL3:8; A4: dist(p,x) < r by A2,A3,METRIC_1:11; A5: |.p1-x1.| = dist(p,x) by SPPOL_1:39; A6: |.p1-a.| <= |.p1-x1.| + |.x1-a.| by TOPRNS_1:34; |.p1-x1.| + |.x1-a.| < s by A4,A5,XREAL_1:6; then |.p1-a.| < s by A6,XXREAL_0:2; hence thesis by TOPREAL9:7; end; theorem for S, T being TopStruct, f being Function of S, T st f is being_homeomorphism holds f is onto; registration let T be non empty T_2 TopSpace; cluster -> T_2 for non empty SubSpace of T; coherence; end; registration let p, r; cluster Tdisk(p,r) -> closed; coherence proof let A be Subset of T2; assume A = the carrier of Tdisk(p,r); then A = cl_Ball(p,r) by BROUWER:3; hence thesis; end; end; registration let p, r; cluster Tdisk(p,r) -> compact; coherence proof set D = Tdisk(p,r); reconsider Q = [#]D as Subset of T2 by TSEP_1:1; [#]D = cl_Ball(p,r) by BROUWER:3; then Q is compact by TOPREAL6:79; then [#]D is compact by COMPTS_1:2; hence thesis by COMPTS_1:1; end; end; begin :: Paths theorem for T being non empty TopSpace, a, b being Point of T for f being Path of a,b st a,b are_connected holds rng f is connected proof let T be non empty TopSpace, a, b be Point of T; let f be Path of a,b such that A1: a,b are_connected; A2: dom f = the carrier of I[01] by FUNCT_2:def 1; reconsider A = [.0,1.] as interval Subset of R^1 by TOPMETR:17; reconsider B = A as Subset of I[01] by BORSUK_1:40; A3: B is connected by CONNSP_1:23; A4: f is continuous by A1,BORSUK_2:def 2; f.:B = rng f by A2,BORSUK_1:40,RELAT_1:113; hence thesis by A3,A4,TOPS_2:61; end; theorem Th29: for X being non empty TopSpace, Y being non empty SubSpace of X, x1, x2 being Point of X, y1, y2 being Point of Y, f being Path of x1,x2 st x1 = y1 & x2 = y2 & x1,x2 are_connected & rng f c= the carrier of Y holds y1,y2 are_connected & f is Path of y1,y2 proof let X be non empty TopSpace, Y be non empty SubSpace of X, x1, x2 be Point of X, y1, y2 be Point of Y, f be Path of x1,x2 such that A1: x1 = y1 and A2: x2 = y2 and A3: x1, x2 are_connected; assume rng f c= the carrier of Y; then reconsider g = f as Function of I[01], Y by FUNCT_2:6; A4: f is continuous by A3,BORSUK_2:def 2; A5: f.0 = y1 & f.1 = y2 by A1,A2,A3,BORSUK_2:def 2; A6: g is continuous by A4,PRE_TOPC:27; thus ex f being Function of I[01], Y st f is continuous & f.0 = y1 & f.1 = y2 proof take g; thus g is continuous by A4,PRE_TOPC:27; thus thesis by A1,A2,A3,BORSUK_2:def 2; end; y1, y2 are_connected by A5,A6; hence thesis by A5,A6,BORSUK_2:def 2; end; theorem Th30: for X being pathwise_connected non empty TopSpace, Y being non empty SubSpace of X, x1, x2 being Point of X, y1, y2 being Point of Y, f being Path of x1,x2 st x1 = y1 & x2 = y2 & rng f c= the carrier of Y holds y1,y2 are_connected & f is Path of y1,y2 proof let X be pathwise_connected non empty TopSpace, Y be non empty SubSpace of X, x1, x2 be Point of X, y1, y2 be Point of Y; x1,x2 are_connected by BORSUK_2:def 3; hence thesis by Th29; end; Lm7: for T being non empty TopSpace, a, b being Point of T for f being Path of a,b st a,b are_connected holds rng f c= rng -f proof let T be non empty TopSpace; let a, b be Point of T; let f be Path of a,b; assume A1: a,b are_connected; let y be object; assume y in rng f; then consider x being object such that A2: x in dom f and A3: f.x = y by FUNCT_1:def 3; reconsider x as Point of I[01] by A2; A4: dom -f = the carrier of I[01] by FUNCT_2:def 1; A5: 1-x is Point of I[01] by JORDAN5B:4; then (-f).(1-x) = f.(1-(1-x)) by A1,BORSUK_2:def 6; hence thesis by A3,A4,A5,FUNCT_1:def 3; end; theorem Th31: for T being non empty TopSpace, a, b being Point of T for f being Path of a,b st a,b are_connected holds rng f = rng -f proof let T be non empty TopSpace; let a, b be Point of T; let f be Path of a,b; assume A1: a,b are_connected; hence rng f c= rng -f by Lm7; f = --f by A1,BORSUK_6:43; hence thesis by A1,Lm7; end; theorem Th32: for T being pathwise_connected non empty TopSpace, a, b being Point of T for f being Path of a,b holds rng f = rng -f by Th31,BORSUK_2:def 3; theorem Th33: for T being non empty TopSpace, a, b, c being Point of T for f being Path of a,b, g being Path of b,c st a,b are_connected & b,c are_connected holds rng f c= rng(f+g) proof let T be non empty TopSpace; let a, b, c be Point of T; let f be Path of a,b; let g be Path of b,c; assume that A1: a,b are_connected and A2: b,c are_connected; let y be object; assume y in rng f; then consider x being object such that A3: x in dom f and A4: f.x = y by FUNCT_1:def 3; A5: dom(f+g) = the carrier of I[01] by FUNCT_2:def 1; reconsider x as Point of I[01] by A3; 1/2*x = x/2; then A6: x/2 is Point of I[01] by BORSUK_6:6; x <= 1 by BORSUK_1:43; then x/2 <= 1/2 by XREAL_1:72; then (f+g).(x/2) = f.(2*(x/2)) by A1,A2,A6,BORSUK_2:def 5; hence thesis by A4,A5,A6,FUNCT_1:def 3; end; theorem for T being pathwise_connected non empty TopSpace, a, b, c being Point of T for f being Path of a,b, g being Path of b,c holds rng f c= rng(f+g) proof let T be pathwise_connected non empty TopSpace; let a, b, c be Point of T; let f be Path of a,b; let g be Path of b,c; A1: a,b are_connected by BORSUK_2:def 3; b,c are_connected by BORSUK_2:def 3; hence thesis by A1,Th33; end; theorem Th35: for T being non empty TopSpace, a, b, c being Point of T for f being Path of b,c, g being Path of a,b st a,b are_connected & b,c are_connected holds rng f c= rng(g+f) proof let T be non empty TopSpace; let a, b, c be Point of T; let f be Path of b,c; let g be Path of a,b; assume that A1: a,b are_connected and A2: b,c are_connected; let y be object; assume y in rng f; then consider x being object such that A3: x in dom f and A4: f.x = y by FUNCT_1:def 3; A5: dom(g+f) = the carrier of I[01] by FUNCT_2:def 1; reconsider x as Point of I[01] by A3; A6: 0 <= x by BORSUK_1:43; then A7: 0+1/2 <= x/2+1/2 by XREAL_1:6; x <= 1 by BORSUK_1:43; then x+1 <= 1+1 by XREAL_1:6; then (x+1)/2 <= 2/2 by XREAL_1:72; then A8: x/2+1/2 is Point of I[01] by A6,BORSUK_1:43; then (g+f).(x/2+1/2) = f.(2*(x/2+1/2)-1) by A1,A2,A7,BORSUK_2:def 5; hence thesis by A4,A5,A8,FUNCT_1:def 3; end; theorem for T being pathwise_connected non empty TopSpace, a, b, c being Point of T for f being Path of b,c, g being Path of a,b holds rng f c= rng(g+f) proof let T be pathwise_connected non empty TopSpace; let a, b, c be Point of T; let f be Path of b,c; let g be Path of a,b; A1: a,b are_connected by BORSUK_2:def 3; b,c are_connected by BORSUK_2:def 3; hence thesis by A1,Th35; end; theorem Th37: for T being non empty TopSpace, a, b, c being Point of T for f being Path of a,b, g being Path of b,c st a,b are_connected & b,c are_connected holds rng(f+g) = rng f \/ rng g proof let T be non empty TopSpace; let a, b, c be Point of T; let f be Path of a,b; let g be Path of b,c; assume that A1: a,b are_connected and A2: b,c are_connected; thus rng(f+g) c= rng f \/ rng g proof let y be object; assume y in rng(f+g); then consider x being object such that A3: x in dom(f+g) and A4: y = (f+g).x by FUNCT_1:def 3; reconsider x as Point of I[01] by A3; per cases; suppose A5: x <= 1/2; then A6: (f+g).x = f.(2*x) by A1,A2,BORSUK_2:def 5; A7: rng f c= rng f \/ rng g by XBOOLE_1:7; A8: dom f = the carrier of I[01] by FUNCT_2:def 1; 2*x is Point of I[01] by A5,BORSUK_6:3; then y in rng f by A4,A6,A8,FUNCT_1:def 3; hence thesis by A7; end; suppose A9: 1/2 <= x; then A10: (f+g).x = g.(2*x-1) by A1,A2,BORSUK_2:def 5; A11: rng g c= rng f \/ rng g by XBOOLE_1:7; A12: dom g = the carrier of I[01] by FUNCT_2:def 1; 2*x-1 is Point of I[01] by A9,BORSUK_6:4; then y in rng g by A4,A10,A12,FUNCT_1:def 3; hence thesis by A11; end; end; A13: rng f c= rng(f+g) by A1,A2,Th33; rng g c= rng(f+g) by A1,A2,Th35; hence thesis by A13,XBOOLE_1:8; end; theorem for T being pathwise_connected non empty TopSpace, a, b, c being Point of T for f being Path of a,b, g being Path of b,c holds rng(f+g) = rng f \/ rng g proof let T be pathwise_connected non empty TopSpace; let a, b, c be Point of T; let f be Path of a,b; let g be Path of b,c; A1: a,b are_connected by BORSUK_2:def 3; b,c are_connected by BORSUK_2:def 3; hence thesis by A1,Th37; end; theorem Th39: for T being non empty TopSpace, a, b, c, d being Point of T for f being Path of a,b, g being Path of b,c, h being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds rng(f+g+h) = rng f \/ rng g \/ rng h proof let T be non empty TopSpace; let a, b, c, d be Point of T; let f be Path of a,b; let g be Path of b,c; let h be Path of c,d; assume that A1: a,b are_connected and A2: b,c are_connected and A3: c,d are_connected; a,c are_connected by A1,A2,BORSUK_6:42; hence rng(f+g+h) = rng(f+g) \/ rng h by A3,Th37 .= rng f \/ rng g \/ rng h by A1,A2,Th37; end; theorem Th40: for T being pathwise_connected non empty TopSpace, a, b, c, d being Point of T for f being Path of a,b, g being Path of b,c, h being Path of c,d holds rng(f+g+h) = rng f \/ rng g \/ rng h proof let T be pathwise_connected non empty TopSpace; let a, b, c, d be Point of T; let f be Path of a,b; let g be Path of b,c; let h be Path of c,d; A1: a,b are_connected by BORSUK_2:def 3; A2: b,c are_connected by BORSUK_2:def 3; c,d are_connected by BORSUK_2:def 3; hence thesis by A1,A2,Th39; end; Lm8: for T being non empty TopSpace, a, b, c, d, e being Point of T for f being Path of a,b, g being Path of b,c, h being Path of c,d, i being Path of d,e st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds rng(f+g+h+i) = rng f \/ rng g \/ rng h \/ rng i proof let T be non empty TopSpace; let a, b, c, d, e be Point of T; let f be Path of a,b; let g be Path of b,c; let h be Path of c,d; let i be Path of d,e; assume that A1: a,b are_connected and A2: b,c are_connected and A3: c,d are_connected and A4: d,e are_connected; a,c are_connected by A1,A2,BORSUK_6:42; then a,d are_connected by A3,BORSUK_6:42; hence rng(f+g+h+i) = rng(f+g+h) \/ rng i by A4,Th37 .= rng f \/ rng g \/ rng h \/ rng i by A1,A2,A3,Th39; end; Lm9: for T being pathwise_connected non empty TopSpace, a, b, c, d, e being Point of T for f being Path of a,b, g being Path of b,c, h being Path of c,d, i being Path of d,e holds rng(f+g+h+i) = rng f \/ rng g \/ rng h \/ rng i proof let T be pathwise_connected non empty TopSpace; let a, b, c, d, e be Point of T; let f be Path of a,b; let g be Path of b,c; let h be Path of c,d; let i be Path of d,e; A1: a,b are_connected by BORSUK_2:def 3; A2: b,c are_connected by BORSUK_2:def 3; A3: c,d are_connected by BORSUK_2:def 3; d,e are_connected by BORSUK_2:def 3; hence thesis by A1,A2,A3,Lm8; end; Lm10: for T being non empty TopSpace, a, b, c, d, e, z being Point of T for f being Path of a,b, g being Path of b,c, h being Path of c,d, i being Path of d,e, j being Path of e,z st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & e,z are_connected holds rng(f+g+h+i+j) = rng f \/ rng g \/ rng h \/ rng i \/ rng j proof let T be non empty TopSpace; let a, b, c, d, e, z be Point of T; let f be Path of a,b; let g be Path of b,c; let h be Path of c,d; let i be Path of d,e; let j be Path of e,z; assume that A1: a,b are_connected and A2: b,c are_connected and A3: c,d are_connected and A4: d,e are_connected and A5: e,z are_connected; a,c are_connected by A1,A2,BORSUK_6:42; then a,d are_connected by A3,BORSUK_6:42; then a,e are_connected by A4,BORSUK_6:42; hence rng(f+g+h+i+j) = rng(f+g+h+i) \/ rng j by A5,Th37 .= rng f \/ rng g \/ rng h \/ rng i \/ rng j by A1,A2,A3,A4,Lm8; end; Lm11: for T being pathwise_connected non empty TopSpace, a, b, c, d, e, z being Point of T for f being Path of a,b, g being Path of b,c, h being Path of c,d, i being Path of d,e, j being Path of e,z holds rng(f+g+h+i+j) = rng f \/ rng g \/ rng h \/ rng i \/ rng j proof let T be pathwise_connected non empty TopSpace; let a, b, c, d, e, z be Point of T; let f be Path of a,b; let g be Path of b,c; let h be Path of c,d; let i be Path of d,e; let j be Path of e,z; A1: a,b are_connected by BORSUK_2:def 3; A2: b,c are_connected by BORSUK_2:def 3; A3: c,d are_connected by BORSUK_2:def 3; A4: d,e are_connected by BORSUK_2:def 3; e,z are_connected by BORSUK_2:def 3; hence thesis by A1,A2,A3,A4,Lm10; end; theorem Th41: for T being non empty TopSpace, a being Point of T holds I[01] --> a is Path of a,a proof let T be non empty TopSpace, a be Point of T; thus a,a are_connected; thus thesis by BORSUK_1:def 14,def 15,TOPALG_3:4; end; theorem Th42: for p1, p2 being Point of TOP-REAL n, P being Subset of TOP-REAL n holds P is_an_arc_of p1,p2 implies ex F being Path of p1,p2, f being Function of I[01], (TOP-REAL n)|P st rng f = P & F = f proof let p1, p2 be Point of TOP-REAL n, P be Subset of TOP-REAL n; assume A1: P is_an_arc_of p1,p2; then reconsider P1 = P as non empty Subset of TOP-REAL n by TOPREAL1:1; consider h being Function of I[01], (TOP-REAL n)|P such that A2: h is being_homeomorphism and A3: h.0 = p1 and A4: h.1 = p2 by A1,TOPREAL1:def 1; h is Function of I[01], (TOP-REAL n)|P1; then reconsider h1 = h as Function of I[01],TOP-REAL n by TOPREALA:7; h1 is continuous by A2,PRE_TOPC:26; then reconsider f = h as Path of p1,p2 by A3,A4,BORSUK_2:def 4; take f, h; thus rng h = [#]((TOP-REAL n)|P) by A2,TOPS_2:def 5 .= P by PRE_TOPC:8; thus thesis; end; theorem Th43: for p1, p2 being Point of TOP-REAL n ex F being Path of p1,p2, f being Function of I[01], (TOP-REAL n)|LSeg(p1,p2) st rng f = LSeg(p1,p2) & F = f proof let p1, p2 be Point of TOP-REAL n; per cases; suppose A1: p1 = p2; then reconsider g = I[01] --> p1 as Path of p1,p2 by Th41; take g; A2: LSeg(p1,p2) = {p1} by A1,RLTOPSP1:70; A3: rng g = {p1} by FUNCOP_1:8; the carrier of (TOP-REAL n)|LSeg(p1,p2) = LSeg(p1,p2) by PRE_TOPC:8; then reconsider f = g as Function of I[01],(TOP-REAL n)|LSeg(p1,p2) by A2,A3,FUNCT_2:6; take f; thus thesis by A1,A3,RLTOPSP1:70; end; suppose p1 <> p2; hence thesis by Th42,TOPREAL1:9; end; end; theorem Th44: for p1,p2,q1,q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 ex f being Path of q1,q2 st rng f c= P & rng f misses {p1,p2} proof let p1,p2,q1,q2 be Point of TOP-REAL 2 such that A1: P is_an_arc_of p1,p2 and A2: q1 in P and A3: q2 in P and A4: q1 <> p1 and A5: q1 <> p2 and A6: q2 <> p1 and A7: q2 <> p2; per cases; suppose q1 = q2; then reconsider f = I[01] --> q1 as Path of q1,q2 by Th41; take f; A8: rng f = {q1} by FUNCOP_1:8; thus rng f c= P by A2,A8,TARSKI:def 1; A9: not p1 in {q1} by A4,TARSKI:def 1; not p2 in {q1} by A5,TARSKI:def 1; hence thesis by A8,A9,ZFMISC_1:51; end; suppose q1 <> q2; then consider Q being non empty Subset of T2 such that A10: Q is_an_arc_of q1,q2 and A11: Q c= P and A12: Q misses {p1,p2} by A1,A2,A3,A4,A5,A6,A7,JORDAN16:23; consider g being Path of q1,q2, f being Function of I[01], T2|Q such that A13: rng f = Q and A14: g = f by A10,Th42; reconsider h = f as Function of I[01],T2 by TOPREALA:7; the carrier of T2|Q = Q by PRE_TOPC:8; then reconsider z1 = q1, z2 = q2 as Point of T2|Q by A10,TOPREAL1:1; A15: z1,z2 are_connected proof take f; thus f is continuous by A14,PRE_TOPC:27; thus thesis by A14,BORSUK_2:def 4; end; A16: f is continuous by A14,PRE_TOPC:27; f.0 =z1 & f.1=z2 by A14,BORSUK_2:def 4; then f is Path of z1,z2 by A15,A16,BORSUK_2:def 2; then reconsider h as Path of q1,q2 by A15,TOPALG_2:1; take h; thus thesis by A11,A12,A13; end; end; begin :: Rectangles theorem Th45: a <= b & c <= d implies rectangle(a,b,c,d) c= closed_inside_of_rectangle(a,b,c,d) proof assume that A1: a <= b and A2: c <= d; let x be object; assume x in rectangle(a,b,c,d); then x in {p: p`1 = a & p`2 <= d & p`2 >= c or p`1 <= b & p`1 >= a & p`2 = d or p`1 <= b & p`1 >= a & p`2 = c or p`1 = b & p`2 <= d & p`2 >= c} by A1,A2,SPPOL_2:54; then ex p st x = p & (p`1 = a & p`2 <= d & p`2 >= c or p`1 <= b & p`1 >= a & p`2 = d or p`1 <= b & p`1 >= a & p`2 = c or p`1 = b & p`2 <= d & p`2 >= c); hence thesis by A1,A2; end; theorem Th46: inside_of_rectangle(a,b,c,d) c= closed_inside_of_rectangle(a,b,c,d) proof let x be object; assume x in inside_of_rectangle(a,b,c,d); then ex p st x = p & a < p`1 & p`1 < b & c < p`2 & p`2 < d; hence thesis; end; theorem Th47: closed_inside_of_rectangle(a,b,c,d) = outside_of_rectangle(a,b,c,d)` proof set R = closed_inside_of_rectangle(a,b,c,d); set O = outside_of_rectangle(a,b,c,d); thus R c= O` proof let x be object; assume x in R; then consider p such that A1: x = p and A2: a <= p`1 and A3: p`1 <= b and A4: c <= p`2 and A5: p`2 <= d; now assume p in O; then ex p1 st p1 = p & not(a <= p1`1 & p1`1 <= b & c <= p1`2 & p1`2 <= d); hence contradiction by A2,A3,A4,A5; end; hence thesis by A1,SUBSET_1:29; end; let x be object; assume A6: x in O`; then A7: not x in O by XBOOLE_0:def 5; reconsider x as Point of T2 by A6; A8: a <= x`1 by A7; A9: x`1 <= b by A7; A10: c <= x`2 by A7; x`2 <= d by A7; hence thesis by A8,A9,A10; end; registration let a, b, c, d be Real; cluster closed_inside_of_rectangle(a,b,c,d) -> closed; coherence proof set P2 = outside_of_rectangle(a,b,c,d); reconsider P2 as open Subset of T2 by JORDAN1:34; P2` is closed; hence thesis by Th47; end; end; theorem Th48: closed_inside_of_rectangle(a,b,c,d) misses outside_of_rectangle(a,b,c,d) proof set R = closed_inside_of_rectangle(a,b,c,d); set P2 = outside_of_rectangle(a,b,c,d); assume R meets P2; then consider x being object such that A1: x in R and A2: x in P2 by XBOOLE_0:3; A3: ex p st x = p & a <= p`1 & p`1 <= b & c <= p`2 & p`2 <= d by A1; ex p st x = p & not (a <= p`1 & p`1 <= b & c <= p`2 & p`2 <= d) by A2; hence thesis by A3; end; theorem Th49: closed_inside_of_rectangle(a,b,c,d) /\ inside_of_rectangle(a,b,c,d) = inside_of_rectangle(a,b,c,d) proof set R = closed_inside_of_rectangle(a,b,c,d); set P1 = inside_of_rectangle(a,b,c,d); thus R /\ P1 c= P1 by XBOOLE_1:17; P1 /\ P1 c= P1 /\ R by Th46,XBOOLE_1:26; hence thesis; end; theorem Th50: a < b & c < d implies Int closed_inside_of_rectangle(a,b,c,d) = inside_of_rectangle(a,b,c,d) proof assume that A1: a < b and A2: c < d; set P = rectangle(a,b,c,d); set R = closed_inside_of_rectangle(a,b,c,d); set P1 = inside_of_rectangle(a,b,c,d); set P2 = outside_of_rectangle(a,b,c,d); A3: P = {p where p is Point of T2: p`1 = a & p`2 <= d & p`2 >= c or p`1 <= b & p`1 >= a & p`2 = d or p`1 <= b & p`1 >= a & p`2 = c or p`1 = b & p`2 <= d & p`2 >= c} by A1,A2,SPPOL_2:54; A4: R misses P2 by Th48; thus Int R = (Cl P2``)` by Th47 .= (P2 \/ P)` by A1,A2,A3,JORDAN1:44 .= P2` /\ P` by XBOOLE_1:53 .= R /\ P` by Th47 .= R /\ (P1 \/ P2) by A1,A2,A3,JORDAN1:36 .= R /\ P1 \/ R /\ P2 by XBOOLE_1:23 .= R /\ P1 \/ {} by A4 .= P1 by Th49; end; theorem Th51: a <= b & c <= d implies closed_inside_of_rectangle(a,b,c,d) \ inside_of_rectangle(a,b,c,d) = rectangle(a,b,c,d) proof assume that A1: a <= b and A2: c <= d; set R = rectangle(a,b,c,d); set P = closed_inside_of_rectangle(a,b,c,d); set P1 = inside_of_rectangle(a,b,c,d); A3: R = {p where p is Point of T2: p`1 = a & p`2 <= d & p`2 >= c or p`1 <= b & p`1 >= a & p`2 = d or p`1 <= b & p`1 >= a & p`2 = c or p`1 = b & p`2 <= d & p`2 >= c} by A1,A2,SPPOL_2:54; thus P \ P1 c= R proof let x be object; assume A4: x in P \ P1; then A5: not x in P1 by XBOOLE_0:def 5; x in P by A4,XBOOLE_0:def 5; then consider p such that A6: x = p and A7: a <= p`1 and A8: p`1 <= b and A9: c <= p`2 and A10: p`2 <= d; not (a < p`1 & p`1 < b & c < p`2 & p`2 < d) by A5,A6; then p`1 = a & p`2 <= d & p`2 >= c or p`1 <= b & p`1 >= a & p`2 = d or p`1 <= b & p`1 >= a & p`2 = c or p`1 = b & p`2 <= d & p`2 >= c by A7,A8,A9,A10,XXREAL_0:1; hence thesis by A3,A6; end; let x be object; assume A11: x in R; then A12: ex p st p = x & (p`1 = a & p`2 <= d & p`2 >= c or p`1 <= b & p`1 >= a & p`2 = d or p`1 <= b & p`1 >= a & p`2 = c or p`1 = b & p`2 <= d & p`2 >= c) by A3; A13: R c= P by A1,A2,Th45; now assume x in P1; then ex p st x = p & a < p`1 & p`1 < b & c < p`2 & p`2 < d; hence contradiction by A12; end; hence thesis by A11,A13,XBOOLE_0:def 5; end; theorem Th52: a < b & c < d implies Fr closed_inside_of_rectangle(a,b,c,d) = rectangle(a,b,c,d) proof assume that A1: a < b and A2: c < d; set P = closed_inside_of_rectangle(a,b,c,d); thus Fr P = P \ Int P by TOPS_1:43 .= P \ inside_of_rectangle(a,b,c,d) by A1,A2,Th50 .= rectangle(a,b,c,d) by A1,A2,Th51; end; theorem a <= b & c <= d implies W-bound closed_inside_of_rectangle(a,b,c,d) = a proof assume that A1: a <= b and A2: c <= d; set X = closed_inside_of_rectangle(a,b,c,d); reconsider Z = (proj1|X).:the carrier of (T2|X) as Subset of REAL; A3: X = the carrier of (T2|X) by PRE_TOPC:8; A4: |[a,c]| in X by A1,A2,TOPREALA:31; A5: for p be Real st p in Z holds p >= a proof let p be Real; assume p in Z; then consider p0 being object such that A6: p0 in the carrier of T2|X and p0 in the carrier of T2|X and A7: p = (proj1|X).p0 by FUNCT_2:64; ex p1 st p0 = p1 & a <= p1`1 & p1`1 <= b & c <= p1`2 & p1`2 <= d by A3,A6; hence thesis by A3,A6,A7,PSCOMP_1:22; end; for q being Real st for p being Real st p in Z holds p >= q holds a >= q proof let q be Real such that A8: for p being Real st p in Z holds p >= q; A9: |[a,c]|`1 = a by EUCLID:52; (proj1|X). |[a,c]| = |[a,c]|`1 by A1,A2,PSCOMP_1:22,TOPREALA:31; hence thesis by A3,A4,A8,A9,FUNCT_2:35; end; hence thesis by A4,A5,SEQ_4:44; end; theorem a <= b & c <= d implies S-bound closed_inside_of_rectangle(a,b,c,d) = c proof assume that A1: a <= b and A2: c <= d; set X = closed_inside_of_rectangle(a,b,c,d); reconsider Z = (proj2|X).:the carrier of (T2|X) as Subset of REAL; A3: X = the carrier of (T2|X) by PRE_TOPC:8; A4: |[a,c]| in X by A1,A2,TOPREALA:31; A5: for p be Real st p in Z holds p >= c proof let p be Real; assume p in Z; then consider p0 being object such that A6: p0 in the carrier of T2|X and p0 in the carrier of T2|X and A7: p = (proj2|X).p0 by FUNCT_2:64; ex p1 st p0 = p1 & a <= p1`1 & p1`1 <= b & c <= p1`2 & p1`2 <= d by A3,A6; hence thesis by A3,A6,A7,PSCOMP_1:23; end; for q being Real st for p being Real st p in Z holds p >= q holds c >= q proof let q be Real such that A8: for p being Real st p in Z holds p >= q; A9: |[a,c]|`2 = c by EUCLID:52; (proj2|X). |[a,c]| = |[a,c]|`2 by A1,A2,PSCOMP_1:23,TOPREALA:31; hence thesis by A3,A4,A8,A9,FUNCT_2:35; end; hence thesis by A4,A5,SEQ_4:44; end; theorem a <= b & c <= d implies E-bound closed_inside_of_rectangle(a,b,c,d) = b proof assume that A1: a <= b and A2: c <= d; set X = closed_inside_of_rectangle(a,b,c,d); reconsider Z = (proj1|X).:the carrier of (T2|X) as Subset of REAL; A3: X = the carrier of (T2|X) by PRE_TOPC:8; A4: for p be Real st p in Z holds p <= b proof let p be Real; assume p in Z; then consider p0 being object such that A5: p0 in the carrier of T2|X and p0 in the carrier of T2|X and A6: p = (proj1|X).p0 by FUNCT_2:64; ex p1 st p0 = p1 & a <= p1`1 & p1`1 <= b & c <= p1`2 & p1`2 <= d by A3,A5; hence thesis by A3,A5,A6,PSCOMP_1:22; end; A7: for q being Real st for p being Real st p in Z holds p <= q holds b <= q proof let q be Real such that A8: for p being Real st p in Z holds p <= q; A9: |[b,d]|`1 = b by EUCLID:52; |[b,d]|`2 = d by EUCLID:52; then A10: |[b,d]| in X by A1,A2,A9; then (proj1|X). |[b,d]| = |[b,d]|`1 by PSCOMP_1:22; hence thesis by A3,A8,A9,A10,FUNCT_2:35; end; |[a,c]| in X by A1,A2,TOPREALA:31; hence thesis by A4,A7,SEQ_4:46; end; theorem a <= b & c <= d implies N-bound closed_inside_of_rectangle(a,b,c,d) = d proof assume that A1: a <= b and A2: c <= d; set X = closed_inside_of_rectangle(a,b,c,d); reconsider Z = (proj2|X).:the carrier of (T2|X) as Subset of REAL; A3: X = the carrier of (T2|X) by PRE_TOPC:8; A4: for p be Real st p in Z holds p <= d proof let p be Real; assume p in Z; then consider p0 being object such that A5: p0 in the carrier of T2|X and p0 in the carrier of T2|X and A6: p = (proj2|X).p0 by FUNCT_2:64; ex p1 st p0 = p1 & a <= p1`1 & p1`1 <= b & c <= p1`2 & p1`2 <= d by A3,A5; hence thesis by A3,A5,A6,PSCOMP_1:23; end; A7: for q being Real st for p being Real st p in Z holds p <= q holds d <= q proof let q be Real such that A8: for p being Real st p in Z holds p <= q; A9: |[b,d]|`1 = b by EUCLID:52; A10: |[b,d]|`2 = d by EUCLID:52; then A11: |[b,d]| in X by A1,A2,A9; then (proj2|X). |[b,d]| = |[b,d]|`2 by PSCOMP_1:23; hence thesis by A3,A8,A10,A11,FUNCT_2:35; end; |[a,c]| in X by A1,A2,TOPREALA:31; hence thesis by A4,A7,SEQ_4:46; end; theorem Th57: a < b & c < d & p1 in closed_inside_of_rectangle(a,b,c,d) & not p2 in closed_inside_of_rectangle(a,b,c,d) & P is_an_arc_of p1,p2 implies Segment(P,p1,p2,p1,First_Point(P,p1,p2,rectangle(a,b,c,d))) c= closed_inside_of_rectangle(a,b,c,d) proof set R = closed_inside_of_rectangle(a,b,c,d); set dR = rectangle(a,b,c,d); set n = First_Point(P,p1,p2,dR); assume that A1: a < b and A2: c < d and A3: p1 in R and A4: not p2 in R and A5: P is_an_arc_of p1,p2; let x be object; assume that A6: x in Segment(P,p1,p2,p1,n) and A7: not x in R; reconsider x as Point of T2 by A6; A8: Fr R = dR by A1,A2,Th52; p1 in P by A5,TOPREAL1:1; then A9: P meets R by A3,XBOOLE_0:3; p2 in P by A5,TOPREAL1:1; then P \ R <> {}T2 by A4,XBOOLE_0:def 5; then A10: P meets dR by A5,A8,A9,CONNSP_1:22,JORDAN6:10; A11: P is closed by A5,JORDAN6:11; then A12: P /\ dR is closed; A13: n in P /\ dR by A5,A10,A11,JORDAN5C:def 1; per cases; suppose x = n; then A14: x in dR by A13,XBOOLE_0:def 4; dR c= R by A1,A2,Th45; hence thesis by A7,A14; end; suppose A15: x <> n; reconsider P as non empty Subset of T2 by A5,TOPREAL1:1; consider f being Function of I[01], T2|P such that A16: f is being_homeomorphism and A17: f.0 = p1 and A18: f.1 = p2 by A5,TOPREAL1:def 1; A19: rng f = [#](T2|P) by A16,TOPS_2:def 5 .= P by PRE_TOPC:def 5; n in P by A13,XBOOLE_0:def 4; then consider na being object such that A20: na in dom f and A21: f.na = n by A19,FUNCT_1:def 3; reconsider na as Real by A20; A22: 0 <= na by A20,BORSUK_1:43; A23: na <= 1 by A20,BORSUK_1:43; A24: Segment(P,p1,p2,p1,n) c= P by JORDAN16:2; then consider xa being object such that A25: xa in dom f and A26: f.xa = x by A6,A19,FUNCT_1:def 3; reconsider xa as Real by A25; A27: 0 <= xa by A25,BORSUK_1:43; A28: xa <= 1 by A25,BORSUK_1:43; A29: Segment(P,p1,p2,p1,x) is_an_arc_of p1,x by A3,A5,A6,A7,A24,JORDAN16:24; then p1 in Segment(P,p1,p2,p1,x) by TOPREAL1:1; then A30: Segment(P,p1,p2,p1,x) meets R by A3,XBOOLE_0:3; x in Segment(P,p1,p2,p1,x) by A29,TOPREAL1:1; then Segment(P,p1,p2,p1,x) \ R <> {}T2 by A7,XBOOLE_0:def 5; then Segment(P,p1,p2,p1,x) meets Fr R by A29,A30,CONNSP_1:22,JORDAN6:10; then consider z being object such that A31: z in Segment(P,p1,p2,p1,x) and A32: z in dR by A8,XBOOLE_0:3; reconsider z as Point of T2 by A31; Segment(P,p1,p2,p1,x) = {p: LE p1,p,P,p1,p2 & LE p,x,P,p1,p2} by JORDAN6:26; then A33: ex zz being Point of T2 st ( zz = z)&( LE p1,zz,P,p1,p2)&( LE zz,x,P,p1,p2) by A31; Segment(P,p1,p2,p1,x) c= P by JORDAN16:2; then consider za being object such that A34: za in dom f and A35: f.za = z by A19,A31,FUNCT_1:def 3; reconsider za as Real by A34; A36: 0 <= za by A34,BORSUK_1:43; A37: za <= 1 by A34,BORSUK_1:43; A38: na <= za by A5,A10,A12,A16,A17,A18,A21,A23,A32,A35,A36,JORDAN5C:def 1; A39: za <= xa by A16,A17,A18,A26,A27,A28,A33,A35,A37,JORDAN5C:def 3; Segment(P,p1,p2,p1,n) = {p: LE p1,p,P,p1,p2 & LE p,n,P,p1,p2} by JORDAN6:26; then ex xx being Point of T2 st ( xx = x)&( LE p1,xx,P,p1,p2)&( LE xx,n,P,p1,p2) by A6; then xa <= na by A16,A17,A18,A21,A22,A23,A26,A28,JORDAN5C:def 3; then xa < na by A15,A21,A26,XXREAL_0:1; hence thesis by A38,A39,XXREAL_0:2; end; end; begin :: Some useful functions definition let S, T be non empty TopSpace, x be Point of [:S,T:]; redefine func x`1 -> Element of S; coherence proof the carrier of [:S,T:] = [:the carrier of S, the carrier of T:] by BORSUK_1:def 2; hence thesis by MCART_1:10; end; redefine func x`2 -> Element of T; coherence proof the carrier of [:S,T:] = [:the carrier of S, the carrier of T:] by BORSUK_1:def 2; hence thesis by MCART_1:10; end; end; definition let o be Point of TOP-REAL 2; func diffX2_1(o) -> RealMap of [:TOP-REAL 2,TOP-REAL 2:] means :Def1: for x being Point of [:TOP-REAL 2,TOP-REAL 2:] holds it.x = x`2`1 - o`1; existence proof deffunc F(Point of [:T2,T2:]) = In($1`2`1 - o`1,REAL); consider xo being RealMap of [:T2,T2:] such that A1: for x being Point of [:T2,T2:] holds xo.x = F(x) from FUNCT_2:sch 4; take xo; let x be Point of [:TOP-REAL 2,TOP-REAL 2:]; xo.x = F(x) by A1; hence thesis; end; uniqueness proof let f, g be RealMap of [:T2,T2:] such that A2: for x being Point of [:T2,T2:] holds f.x = x`2`1 - o`1 and A3: for x being Point of [:T2,T2:] holds g.x = x`2`1 - o`1; now let x be Point of [:T2,T2:]; thus f.x = x`2`1 - o`1 by A2 .= g.x by A3; end; hence thesis by FUNCT_2:63; end; func diffX2_2(o) -> RealMap of [:TOP-REAL 2,TOP-REAL 2:] means :Def2: for x being Point of [:TOP-REAL 2,TOP-REAL 2:] holds it.x = x`2`2 - o`2; existence proof deffunc F(Point of [:T2,T2:]) = In($1`2`2 - o`2,REAL); consider xo being RealMap of [:T2,T2:] such that A4: for x being Point of [:T2,T2:] holds xo.x = F(x) from FUNCT_2:sch 4; take xo; let x be Point of [:TOP-REAL 2,TOP-REAL 2:]; xo.x = F(x) by A4; hence thesis; end; uniqueness proof let f, g be RealMap of [:T2,T2:] such that A5: for x being Point of [:T2,T2:] holds f.x = x`2`2 - o`2 and A6: for x being Point of [:T2,T2:] holds g.x = x`2`2 - o`2; now let x be Point of [:T2,T2:]; thus f.x = x`2`2 - o`2 by A5 .= g.x by A6; end; hence thesis by FUNCT_2:63; end; end; definition func diffX1_X2_1 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means :Def3: for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`1`1 - x`2`1; existence proof deffunc F(Point of [:T2,T2:]) = In($1`1`1 - $1`2`1,REAL); consider xo being RealMap of [:T2,T2:] such that A1: for x being Point of [:T2,T2:] holds xo.x = F(x) from FUNCT_2:sch 4; take xo; let x be Point of [:TOP-REAL 2, TOP-REAL 2:]; xo.x = F(x) by A1; hence thesis; end; uniqueness proof let f, g be RealMap of [:T2,T2:] such that A2: for x being Point of [:T2,T2:] holds f.x = x`1`1 - x`2`1 and A3: for x being Point of [:T2,T2:] holds g.x = x`1`1 - x`2`1; now let x be Point of [:T2,T2:]; thus f.x = x`1`1 - x`2`1 by A2 .= g.x by A3; end; hence thesis by FUNCT_2:63; end; func diffX1_X2_2 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means :Def4: for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`1`2 - x`2`2; existence proof deffunc F(Point of [:T2,T2:]) = In($1`1`2 - $1`2`2,REAL); consider xo being RealMap of [:T2,T2:] such that A4: for x being Point of [:T2,T2:] holds xo.x = F(x) from FUNCT_2:sch 4; take xo; let x be Point of [:TOP-REAL 2, TOP-REAL 2:]; xo.x = F(x) by A4; hence thesis; end; uniqueness proof let f, g be RealMap of [:T2,T2:] such that A5: for x being Point of [:T2,T2:] holds f.x = x`1`2 - x`2`2 and A6: for x being Point of [:T2,T2:] holds g.x = x`1`2 - x`2`2; now let x be Point of [:T2,T2:]; thus f.x = x`1`2 - x`2`2 by A5 .= g.x by A6; end; hence thesis by FUNCT_2:63; end; func Proj2_1 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means :Def5: for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`2`1; existence proof deffunc F(Point of [:T2,T2:]) = In($1`2`1,REAL); consider xo being RealMap of [:T2,T2:] such that A7: for x being Point of [:T2,T2:] holds xo.x = F(x) from FUNCT_2:sch 4; take xo; let x be Point of [:TOP-REAL 2, TOP-REAL 2:]; xo.x = F(x) by A7; hence thesis; end; uniqueness proof let f, g be RealMap of [:T2,T2:] such that A8: for x being Point of [:T2,T2:] holds f.x = x`2`1 and A9: for x being Point of [:T2,T2:] holds g.x = x`2`1; now let x be Point of [:T2,T2:]; thus f.x = x`2`1 by A8 .= g.x by A9; end; hence thesis by FUNCT_2:63; end; func Proj2_2 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means :Def6: for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`2`2; existence proof deffunc F(Point of [:T2,T2:]) = In($1`2`2,REAL); consider xo being RealMap of [:T2,T2:] such that A10: for x being Point of [:T2,T2:] holds xo.x = F(x) from FUNCT_2:sch 4; take xo; let x be Point of [:TOP-REAL 2, TOP-REAL 2:]; xo.x = F(x) by A10; hence thesis; end; uniqueness proof let f, g be RealMap of [:T2,T2:] such that A11: for x being Point of [:T2,T2:] holds f.x = x`2`2 and A12: for x being Point of [:T2,T2:] holds g.x = x`2`2; now let x be Point of [:T2,T2:]; thus f.x = x`2`2 by A11 .= g.x by A12; end; hence thesis by FUNCT_2:63; end; end; theorem Th58: for o being Point of TOP-REAL 2 holds diffX2_1(o) is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1 proof let o be Point of TOP-REAL 2; reconsider Xo = diffX2_1(o) as Function of [:T2,T2:],R^1 by TOPMETR:17; for p being Point of [:T2,T2:], V being Subset of R^1 st Xo.p in V & V is open holds ex W being Subset of [:T2,T2:] st p in W & W is open & Xo.:W c= V proof let p be Point of [:T2,T2:], V be Subset of R^1 such that A1: Xo.p in V and A2: V is open; A3: Xo.p = p`2`1 - o`1 by Def1; set r = p`2`1 - o`1; reconsider V1 = V as open Subset of REAL by A2,BORSUK_5:39,TOPMETR:17; consider g being Real such that A4: 0 < g and A5: ].r-g,r+g.[ c= V1 by A1,A3,RCOMP_1:19; reconsider g as Element of REAL by XREAL_0:def 1; set W2 = {|[x,y]| where x, y is Real: p`2`1-g < x & x < p`2`1+g}; W2 c= the carrier of T2 proof let a be object; assume a in W2; then ex x, y being Real st a = |[x,y]| & p`2`1-g < x & x < p`2`1+g; hence thesis; end; then reconsider W2 as Subset of T2; take [:[#]T2,W2:]; A6: p`2 = |[p`2`1,p`2`2]| by EUCLID:53; A7: p = [p`1,p`2] by Lm5,MCART_1:21; A8: p`2`1-g < p`2`1-0 by A4,XREAL_1:15; p`2`1+0 < p`2`1+g by A4,XREAL_1:6; then p`2 in W2 by A6,A8; hence p in [:[#]T2,W2:] by A7,ZFMISC_1:def 2; W2 is open by PSCOMP_1:19; hence [:[#]T2,W2:] is open by BORSUK_1:6; let b be object; assume b in Xo.:[:[#]T2,W2:]; then consider a being Point of [:T2,T2:] such that A9: a in [:[#]T2,W2:] and A10: Xo.a = b by FUNCT_2:65; A11: a = [a`1,a`2] by Lm5,MCART_1:21; A12: (diffX2_1(o)).a = a`2`1 - o`1 by Def1; a`2 in W2 by A9,A11,ZFMISC_1:87; then consider x2, y2 being Real such that A13: a`2 = |[x2,y2]| and A14: p`2`1-g < x2 and A15: x2 < p`2`1+g; A16: a`2`1 = x2 by A13,EUCLID:52; then A17: p`2`1 - g - o`1 < a`2`1 - o`1 by A14,XREAL_1:9; a`2`1 - o`1 < p`2`1 + g - o`1 by A15,A16,XREAL_1:9; then a`2`1 - o`1 in ].r-g,r+g.[ by A17,XXREAL_1:4; hence thesis by A5,A10,A12; end; hence thesis by JGRAPH_2:10; end; theorem Th59: for o being Point of TOP-REAL 2 holds diffX2_2(o) is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1 proof let o be Point of TOP-REAL 2; reconsider Yo = diffX2_2(o) as Function of [:T2,T2:],R^1 by TOPMETR:17; for p being Point of [:T2,T2:], V being Subset of R^1 st Yo.p in V & V is open holds ex W being Subset of [:T2,T2:] st p in W & W is open & Yo.:W c= V proof let p be Point of [:T2,T2:], V be Subset of R^1 such that A1: Yo.p in V and A2: V is open; A3: p = [p`1,p`2] by Lm5,MCART_1:21; A4: Yo.p = p`2`2 - o`2 by Def2; set r = p`2`2 - o`2; reconsider V1 = V as open Subset of REAL by A2,BORSUK_5:39,TOPMETR:17; consider g being Real such that A5: 0 < g and A6: ].r-g,r+g.[ c= V1 by A1,A4,RCOMP_1:19; reconsider g as Element of REAL by XREAL_0:def 1; set W2 = {|[x,y]| where x, y is Real: p`2`2-g < y & y < p`2`2+g}; W2 c= the carrier of T2 proof let a be object; assume a in W2; then ex x, y being Real st a = |[x,y]| & p`2`2-g < y & y < p`2`2+g; hence thesis; end; then reconsider W2 as Subset of T2; take [:[#]T2,W2:]; A7: p`2 = |[p`2`1,p`2`2]| by EUCLID:53; A8: p`2`2-g < p`2`2-0 by A5,XREAL_1:15; p`2`2+0 < p`2`2+g by A5,XREAL_1:6; then p`2 in W2 by A7,A8; hence p in [:[#]T2,W2:] by A3,ZFMISC_1:def 2; W2 is open by PSCOMP_1:21; hence [:[#]T2,W2:] is open by BORSUK_1:6; let b be object; assume b in Yo.:[:[#]T2,W2:]; then consider a being Point of [:T2,T2:] such that A9: a in [:[#]T2,W2:] and A10: Yo.a = b by FUNCT_2:65; A11: a = [a`1,a`2] by Lm5,MCART_1:21; A12: (diffX2_2(o)).a = a`2`2 - o`2 by Def2; a`2 in W2 by A9,A11,ZFMISC_1:87; then consider x2, y2 being Real such that A13: a`2 = |[x2,y2]| and A14: p`2`2-g < y2 and A15: y2 < p`2`2+g; A16: a`2`2 = y2 by A13,EUCLID:52; then A17: p`2`2 - g - o`2 < a`2`2 - o`2 by A14,XREAL_1:9; a`2`2 - o`2 < p`2`2 + g - o`2 by A15,A16,XREAL_1:9; then a`2`2 - o`2 in ].r-g,r+g.[ by A17,XXREAL_1:4; hence thesis by A6,A10,A12; end; hence thesis by JGRAPH_2:10; end; theorem Th60: diffX1_X2_1 is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1 proof reconsider Dx = diffX1_X2_1 as Function of [:T2,T2:],R^1 by TOPMETR:17; for p being Point of [:T2,T2:], V being Subset of R^1 st Dx.p in V & V is open holds ex W being Subset of [:T2,T2:] st p in W & W is open & Dx.:W c= V proof let p be Point of [:T2,T2:], V be Subset of R^1 such that A1: Dx.p in V and A2: V is open; A3: p = [p`1,p`2] by Lm5,MCART_1:21; A4: diffX1_X2_1.p = p`1`1 - p`2`1 by Def3; set r = p`1`1 - p`2`1; reconsider V1 = V as open Subset of REAL by A2,BORSUK_5:39,TOPMETR:17; consider g being Real such that A5: 0 < g and A6: ].r-g,r+g.[ c= V1 by A1,A4,RCOMP_1:19; reconsider g as Element of REAL by XREAL_0:def 1; set W1 = {|[x,y]| where x, y is Real: p`1`1-g/2 < x & x < p`1`1+g/2}; set W2 = {|[x,y]| where x, y is Real: p`2`1-g/2 < x & x < p`2`1+g/2}; W1 c= the carrier of T2 proof let a be object; assume a in W1; then ex x, y being Real st a = |[x,y]| & p`1`1-g/2 < x & x < p`1`1+g/2; hence thesis; end; then reconsider W1 as Subset of T2; W2 c= the carrier of T2 proof let a be object; assume a in W2; then ex x, y being Real st a = |[x,y]| & p`2`1-g/2 < x & x < p`2`1+g/2; hence thesis; end; then reconsider W2 as Subset of T2; take [:W1,W2:]; A7: p`1 = |[p`1`1,p`1`2]| by EUCLID:53; A8: 0/2 < g/2 by A5,XREAL_1:74; then A9: p`1`1-g/2 < p`1`1-0 by XREAL_1:15; p`1`1+0 < p`1`1+g/2 by A8,XREAL_1:6; then A10: p`1 in W1 by A7,A9; A11: p`2 = |[p`2`1,p`2`2]| by EUCLID:53; A12: p`2`1-g/2 < p`2`1-0 by A8,XREAL_1:15; p`2`1+0 < p`2`1+g/2 by A8,XREAL_1:6; then p`2 in W2 by A11,A12; hence p in [:W1,W2:] by A3,A10,ZFMISC_1:def 2; A13: W1 is open by PSCOMP_1:19; W2 is open by PSCOMP_1:19; hence [:W1,W2:] is open by A13,BORSUK_1:6; let b be object; assume b in Dx.:[:W1,W2:]; then consider a being Point of [:T2,T2:] such that A14: a in [:W1,W2:] and A15: Dx.a = b by FUNCT_2:65; A16: a = [a`1,a`2] by Lm5,MCART_1:21; A17: diffX1_X2_1.a = a`1`1 - a`2`1 by Def3; a`1 in W1 by A14,A16,ZFMISC_1:87; then consider x1, y1 being Real such that A18: a`1 = |[x1,y1]| and A19: p`1`1-g/2 < x1 and A20: x1 < p`1`1+g/2; A21: a`1`1 = x1 by A18,EUCLID:52; A22: p`1`1-g/2+g/2 < x1+g/2 by A19,XREAL_1:6; A23: p`1`1-x1 > p`1`1-(p`1`1+g/2) by A20,XREAL_1:15; A24: p`1`1-x1 < x1+g/2-x1 by A22,XREAL_1:9; p`1`1-x1 > -g/2 by A23; then A25: |.p`1`1-x1.| < g/2 by A24,SEQ_2:1; a`2 in W2 by A14,A16,ZFMISC_1:87; then consider x2, y2 being Real such that A26: a`2 = |[x2,y2]| and A27: p`2`1-g/2 < x2 and A28: x2 < p`2`1+g/2; A29: a`2`1 = x2 by A26,EUCLID:52; A30: p`2`1-g/2+g/2 < x2+g/2 by A27,XREAL_1:6; A31: p`2`1-x2 > p`2`1-(p`2`1+g/2) by A28,XREAL_1:15; A32: p`2`1-x2 < x2+g/2-x2 by A30,XREAL_1:9; p`2`1-x2 > -g/2 by A31; then |.p`2`1-x2.| < g/2 by A32,SEQ_2:1; then A33: |.p`1`1-x1.|+|.p`2`1-x2.| < g/2+g/2 by A25,XREAL_1:8; |.p`1`1-x1-(p`2`1-x2).| <= |.p`1`1-x1.|+|.p`2`1-x2.| by COMPLEX1:57; then |.-(p`1`1-x1-(p`2`1-x2)).| <= |.p`1`1-x1.|+|.p`2`1-x2.| by COMPLEX1:52; then |.x1-x2-r.| < g by A33,XXREAL_0:2; then a`1`1 - a`2`1 in ].r-g,r+g.[ by A21,A29,RCOMP_1:1; hence thesis by A6,A15,A17; end; hence thesis by JGRAPH_2:10; end; theorem Th61: diffX1_X2_2 is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1 proof reconsider Dy = diffX1_X2_2 as Function of [:T2,T2:],R^1 by TOPMETR:17; for p being Point of [:T2,T2:], V being Subset of R^1 st Dy.p in V & V is open holds ex W being Subset of [:T2,T2:] st p in W & W is open & Dy.:W c= V proof let p be Point of [:T2,T2:], V be Subset of R^1 such that A1: Dy.p in V and A2: V is open; A3: p = [p`1,p`2] by Lm5,MCART_1:21; A4: diffX1_X2_2.p = p`1`2 - p`2`2 by Def4; set r = p`1`2 - p`2`2; reconsider V1 = V as open Subset of REAL by A2,BORSUK_5:39,TOPMETR:17; consider g being Real such that A5: 0 < g and A6: ].r-g,r+g.[ c= V1 by A1,A4,RCOMP_1:19; reconsider g as Element of REAL by XREAL_0:def 1; set W1 = {|[x,y]| where x, y is Real: p`1`2-g/2 < y & y < p`1`2+g/2}; set W2 = {|[x,y]| where x, y is Real: p`2`2-g/2 < y & y < p`2`2+g/2}; W1 c= the carrier of T2 proof let a be object; assume a in W1; then ex x, y being Real st a = |[x,y]| & p`1`2-g/2 < y & y < p`1`2+g/2; hence thesis; end; then reconsider W1 as Subset of T2; W2 c= the carrier of T2 proof let a be object; assume a in W2; then ex x, y being Real st a = |[x,y]| & p`2`2-g/2 < y & y < p`2`2+g/2; hence thesis; end; then reconsider W2 as Subset of T2; take [:W1,W2:]; A7: p`1 = |[p`1`1,p`1`2]| by EUCLID:53; A8: 0/2 < g/2 by A5,XREAL_1:74; then A9: p`1`2-g/2 < p`1`2-0 by XREAL_1:15; p`1`2+0 < p`1`2+g/2 by A8,XREAL_1:6; then A10: p`1 in W1 by A7,A9; A11: p`2 = |[p`2`1,p`2`2]| by EUCLID:53; A12: p`2`2-g/2 < p`2`2-0 by A8,XREAL_1:15; p`2`2+0 < p`2`2+g/2 by A8,XREAL_1:6; then p`2 in W2 by A11,A12; hence p in [:W1,W2:] by A3,A10,ZFMISC_1:def 2; A13: W1 is open by PSCOMP_1:21; W2 is open by PSCOMP_1:21; hence [:W1,W2:] is open by A13,BORSUK_1:6; let b be object; assume b in Dy.:[:W1,W2:]; then consider a being Point of [:T2,T2:] such that A14: a in [:W1,W2:] and A15: Dy.a = b by FUNCT_2:65; A16: a = [a`1,a`2] by Lm5,MCART_1:21; A17: diffX1_X2_2.a = a`1`2 - a`2`2 by Def4; a`1 in W1 by A14,A16,ZFMISC_1:87; then consider x1, y1 being Real such that A18: a`1 = |[x1,y1]| and A19: p`1`2-g/2 < y1 and A20: y1 < p`1`2+g/2; A21: a`1`2 = y1 by A18,EUCLID:52; A22: p`1`2-g/2+g/2 < y1+g/2 by A19,XREAL_1:6; A23: p`1`2-y1 > p`1`2-(p`1`2+g/2) by A20,XREAL_1:15; A24: p`1`2-y1 < y1+g/2-y1 by A22,XREAL_1:9; p`1`2-y1 > -g/2 by A23; then A25: |.p`1`2-y1.| < g/2 by A24,SEQ_2:1; a`2 in W2 by A14,A16,ZFMISC_1:87; then consider x2, y2 being Real such that A26: a`2 = |[x2,y2]| and A27: p`2`2-g/2 < y2 and A28: y2 < p`2`2+g/2; A29: a`2`2 = y2 by A26,EUCLID:52; A30: p`2`2-g/2+g/2 < y2+g/2 by A27,XREAL_1:6; A31: p`2`2-y2 > p`2`2-(p`2`2+g/2) by A28,XREAL_1:15; A32: p`2`2-y2 < y2+g/2-y2 by A30,XREAL_1:9; p`2`2-y2 > -g/2 by A31; then |.p`2`2-y2.| < g/2 by A32,SEQ_2:1; then A33: |.p`1`2-y1.|+|.p`2`2-y2.| < g/2+g/2 by A25,XREAL_1:8; |.p`1`2-y1-(p`2`2-y2).| <= |.p`1`2-y1.|+|.p`2`2-y2.| by COMPLEX1:57; then |.-(p`1`2-y1-(p`2`2-y2)).| <= |.p`1`2-y1.|+|.p`2`2-y2.| by COMPLEX1:52; then |.y1-y2-r.| < g by A33,XXREAL_0:2; then a`1`2 - a`2`2 in ].r-g,r+g.[ by A21,A29,RCOMP_1:1; hence thesis by A6,A15,A17; end; hence thesis by JGRAPH_2:10; end; theorem Th62: Proj2_1 is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1 proof reconsider fX2 = Proj2_1 as Function of [:T2,T2:],R^1 by TOPMETR:17; for p being Point of [:T2,T2:], V being Subset of R^1 st fX2.p in V & V is open holds ex W being Subset of [:T2,T2:] st p in W & W is open & fX2.:W c= V proof let p be Point of [:T2,T2:], V be Subset of R^1 such that A1: fX2.p in V and A2: V is open; A3: p = [p`1,p`2] by Lm5,MCART_1:21; A4: fX2.p = p`2`1 by Def5; reconsider V1 = V as open Subset of REAL by A2,BORSUK_5:39,TOPMETR:17; consider g being Real such that A5: 0 < g and A6: ].p`2`1-g,p`2`1+g.[ c= V1 by A1,A4,RCOMP_1:19; reconsider g as Element of REAL by XREAL_0:def 1; set W1 = {|[x,y]| where x, y is Real: p`2`1-g < x & x < p`2`1+g}; W1 c= the carrier of T2 proof let a be object; assume a in W1; then ex x, y being Real st a = |[x,y]| & p`2`1-g < x & x < p`2`1+g; hence thesis; end; then reconsider W1 as Subset of T2; take [:[#]T2,W1:]; A7: p`2 = |[p`2`1,p`2`2]| by EUCLID:53; A8: p`2`1-g < p`2`1-0 by A5,XREAL_1:15; p`2`1+0 < p`2`1+g by A5,XREAL_1:6; then p`2 in W1 by A7,A8; hence p in [:[#]T2,W1:] by A3,ZFMISC_1:def 2; W1 is open by PSCOMP_1:19; hence [:[#]T2,W1:] is open by BORSUK_1:6; let b be object; assume b in fX2.:[:[#]T2,W1:]; then consider a being Point of [:T2,T2:] such that A9: a in [:[#]T2,W1:] and A10: fX2.a = b by FUNCT_2:65; A11: a = [a`1,a`2] by Lm5,MCART_1:21; A12: fX2.a = a`2`1 by Def5; a`2 in W1 by A9,A11,ZFMISC_1:87; then consider x1, y1 being Real such that A13: a`2 = |[x1,y1]| and A14: p`2`1-g < x1 and A15: x1 < p`2`1+g; A16: a`2`1 = x1 by A13,EUCLID:52; A17: p`2`1-g+g < x1+g by A14,XREAL_1:6; A18: p`2`1-x1 > p`2`1-(p`2`1+g) by A15,XREAL_1:15; A19: p`2`1-x1 < x1+g-x1 by A17,XREAL_1:9; p`2`1-x1 > -g by A18; then |.p`2`1-x1.| < g by A19,SEQ_2:1; then |.-(p`2`1-x1).| < g by COMPLEX1:52; then |.x1-p`2`1.| < g; then a`2`1 in ].p`2`1-g,p`2`1+g.[ by A16,RCOMP_1:1; hence thesis by A6,A10,A12; end; hence thesis by JGRAPH_2:10; end; theorem Th63: Proj2_2 is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1 proof reconsider fY2 = Proj2_2 as Function of [:T2,T2:],R^1 by TOPMETR:17; for p being Point of [:T2,T2:], V being Subset of R^1 st fY2.p in V & V is open holds ex W being Subset of [:T2,T2:] st p in W & W is open & fY2.:W c= V proof let p be Point of [:T2,T2:], V be Subset of R^1 such that A1: fY2.p in V and A2: V is open; A3: p = [p`1,p`2] by Lm5,MCART_1:21; A4: fY2.p = p`2`2 by Def6; reconsider V1 = V as open Subset of REAL by A2,BORSUK_5:39,TOPMETR:17; consider g being Real such that A5: 0 < g and A6: ].p`2`2-g,p`2`2+g.[ c= V1 by A1,A4,RCOMP_1:19; reconsider g as Element of REAL by XREAL_0:def 1; set W1 = {|[x,y]| where x, y is Real: p`2`2-g < y & y < p`2`2+g}; W1 c= the carrier of T2 proof let a be object; assume a in W1; then ex x, y being Real st a = |[x,y]| & p`2`2-g < y & y < p`2`2+g; hence thesis; end; then reconsider W1 as Subset of T2; take [:[#]T2,W1:]; A7: p`2 = |[p`2`1,p`2`2]| by EUCLID:53; A8: p`2`2-g < p`2`2-0 by A5,XREAL_1:15; p`2`2+0 < p`2`2+g by A5,XREAL_1:6; then p`2 in W1 by A7,A8; hence p in [:[#]T2,W1:] by A3,ZFMISC_1:def 2; W1 is open by PSCOMP_1:21; hence [:[#]T2,W1:] is open by BORSUK_1:6; let b be object; assume b in fY2.:[:[#]T2,W1:]; then consider a being Point of [:T2,T2:] such that A9: a in [:[#]T2,W1:] and A10: fY2.a = b by FUNCT_2:65; A11: a = [a`1,a`2] by Lm5,MCART_1:21; A12: fY2.a = a`2`2 by Def6; a`2 in W1 by A9,A11,ZFMISC_1:87; then consider x1, y1 being Real such that A13: a`2 = |[x1,y1]| and A14: p`2`2-g < y1 and A15: y1 < p`2`2+g; A16: a`2`2 = y1 by A13,EUCLID:52; A17: p`2`2-g+g < y1+g by A14,XREAL_1:6; A18: p`2`2-y1 > p`2`2-(p`2`2+g) by A15,XREAL_1:15; A19: p`2`2-y1 < y1+g-y1 by A17,XREAL_1:9; p`2`2-y1 > -g by A18; then |.p`2`2-y1.| < g by A19,SEQ_2:1; then |.-(p`2`2-y1).| < g by COMPLEX1:52; then |.y1-p`2`2.| < g; then a`2`2 in ].p`2`2-g,p`2`2+g.[ by A16,RCOMP_1:1; hence thesis by A6,A10,A12; end; hence thesis by JGRAPH_2:10; end; registration let o be Point of TOP-REAL 2; cluster diffX2_1(o) -> continuous; coherence proof diffX2_1(o) is continuous Function of [:T2,T2:],R^1 by Th58; hence thesis by JORDAN5A:27; end; cluster diffX2_2(o) -> continuous; coherence proof diffX2_2(o) is continuous Function of [:T2,T2:],R^1 by Th59; hence thesis by JORDAN5A:27; end; end; registration cluster diffX1_X2_1 -> continuous; coherence by Th60,JORDAN5A:27; cluster diffX1_X2_2 -> continuous; coherence by Th61,JORDAN5A:27; cluster Proj2_1 -> continuous; coherence by Th62,JORDAN5A:27; cluster Proj2_2 -> continuous; coherence by Th63,JORDAN5A:27; end; definition let n be non zero Element of NAT, o, p be Point of TOP-REAL n, r be positive Real such that A1: p is Point of Tdisk(o,r); set X = (TOP-REAL n)|(cl_Ball(o,r)\{p}); func DiskProj(o,r,p) -> Function of (TOP-REAL n)|(cl_Ball(o,r)\{p}), Tcircle(o,r) means :Def7: for x being Point of (TOP-REAL n)|(cl_Ball(o,r)\{p}) ex y being Point of TOP-REAL n st x = y & it.x = HC(p,y,o,r); existence proof A2: the carrier of X = cl_Ball(o,r)\{p} by PRE_TOPC:8; defpred P[object,object] means ex z being Point of TOP-REAL n st $1 = z & $2 = HC(p,z,o,r); A3: for x being object st x in the carrier of X ex y being object st y in the carrier of Tcircle(o,r) & P[x,y] proof let x be object such that A4: x in the carrier of X; reconsider z = x as Point of TOP-REAL n by A4,PRE_TOPC:25; z in cl_Ball(o,r) by A2,A4,XBOOLE_0:def 5; then A5: z is Point of Tdisk(o,r) by BROUWER:3; p <> z by A2,A4,ZFMISC_1:56; then HC(p,z,o,r) is Point of Tcircle(o,r) by A1,A5,BROUWER:6; hence thesis; end; consider f being Function of the carrier of X, the carrier of Tcircle(o,r) such that A6: for x being object st x in the carrier of X holds P[x,f.x] from FUNCT_2:sch 1(A3); reconsider f as Function of X, Tcircle(o,r); take f; let x be Point of X; thus thesis by A6; end; uniqueness proof let f, g be Function of X, Tcircle(o,r) such that A7: for x being Point of X ex y being Point of TOP-REAL n st x = y & f.x = HC(p,y,o,r) and A8: for x being Point of X ex y being Point of TOP-REAL n st x = y & g.x = HC(p,y,o,r); now let x be object such that A9: x in the carrier of X; A10: ex y being Point of TOP-REAL n st x = y & f.x = HC(p,y,o,r) by A7,A9; ex y being Point of TOP-REAL n st x = y & g.x = HC(p,y,o,r) by A8,A9; hence f.x = g.x by A10; end; hence thesis by FUNCT_2:12; end; end; theorem Th64: for o, p being Point of TOP-REAL 2, r being positive Real st p is Point of Tdisk(o,r) holds DiskProj(o,r,p) is continuous proof let o, p be Point of TOP-REAL 2; let r be positive Real such that A1: p is Point of Tdisk(o,r); set D = Tdisk(o,r); set cB = cl_Ball(o,r); set Bp = cB \ {p}; set OK = [:Bp,{p}:]; set D1 = T2|Bp; set D2 = T2|{p}; set S1 = Tcircle(o,r); A2: p in {p} by TARSKI:def 1; A3: the carrier of D = cl_Ball(o,r) by BROUWER:3; A4: the carrier of D1 = Bp by PRE_TOPC:8; A5: the carrier of D2 = {p} by PRE_TOPC:8; set TD = [:T2,T2:] | OK; set gg = DiskProj(o,r,p); set xo = diffX2_1(o); set yo = diffX2_2(o); set dx = diffX1_X2_1; set dy = diffX1_X2_2; set fx2 = Proj2_1; set fy2 = Proj2_2; reconsider rr = r^2 as Element of REAL by XREAL_0:def 1; set f1 = (the carrier of [:T2,T2:]) --> rr; reconsider f1 as continuous RealMap of [:T2,T2:] by Lm6; set Zf1 = f1 | OK; set Zfx2 = fx2 | OK; set Zfy2 = fy2 | OK; set Zdx = dx | OK; set Zdy = dy | OK; set Zxo = xo | OK; set Zyo = yo | OK; set xx = Zxo(#)Zdx; set yy = Zyo(#)Zdy; set m = Zdx(#)Zdx + Zdy(#)Zdy; A6: the carrier of TD = OK by PRE_TOPC:8; A7: for y being Point of D1, z being Point of D2 holds Zdx. [y,z] = dx. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A4,A5,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; A8: for y being Point of D1, z being Point of D2 holds Zdy. [y,z] = dy. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A4,A5,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; A9: for y being Point of D1, z being Point of D2 holds Zfx2. [y,z] = fx2. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A4,A5,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; A10: for y being Point of D1, z being Point of D2 holds Zfy2. [y,z] = fy2. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A4,A5,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; A11: for y being Point of D1, z being Point of D2 holds Zf1. [y,z] = f1. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A4,A5,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; A12: for y being Point of D1, z being Point of D2 holds Zxo. [y,z] = xo. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A4,A5,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; A13: for y being Point of D1, z being Point of D2 holds Zyo. [y,z] = yo. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A4,A5,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; now let b be Real; assume b in rng m; then consider a being object such that A14: a in dom m and A15: m.a = b by FUNCT_1:def 3; consider y, z being object such that A16: y in Bp and A17: z in {p} and A18: a = [y,z] by A14,ZFMISC_1:def 2; A19: z = p by A17,TARSKI:def 1; reconsider y, z as Point of T2 by A16,A17; A20: y <> z by A16,A19,ZFMISC_1:56; A21: dx. [y,z] = [y,z]`1`1 - [y,z]`2`1 by Def3; A22: dy. [y,z] = [y,z]`1`2 - [y,z]`2`2 by Def4; set r1 = y`1-z`1; set r2 = y`2-z`2; A23: Zdx. [y,z] = dx. [y,z] by A4,A5,A7,A16,A17; A24: Zdy. [y,z] = dy. [y,z] by A4,A5,A8,A16,A17; dom m c= the carrier of TD by RELAT_1:def 18; then a in the carrier of TD by A14; then A25: m. [y,z] = (Zdx(#)Zdx). [y,z] + (Zdy(#)Zdy). [y,z] by A18,VALUED_1:1 .= Zdx. [y,z] * Zdx. [y,z] + (Zdy(#)Zdy). [y,z] by VALUED_1:5 .= r1^2+r2^2 by A21,A22,A23,A24,VALUED_1:5; now assume A26: r1^2+r2^2 = 0; then A27: r1 = 0 by COMPLEX1:1; r2 = 0 by A26,COMPLEX1:1; hence contradiction by A20,A27,TOPREAL3:6; end; hence 0 < b by A15,A18,A25; end; then reconsider m as positive-yielding continuous RealMap of TD by PARTFUN3:def 1; set p1 = (xx+yy)(#)(xx+yy); set p2 = Zxo(#)Zxo + Zyo(#)Zyo - Zf1; A28: dom p2 = the carrier of TD by FUNCT_2:def 1; now let b be Real; assume b in rng p2; then consider a being object such that A29: a in dom p2 and A30: p2.a = b by FUNCT_1:def 3; consider y, z being object such that A31: y in Bp and A32: z in {p} and A33: a = [y,z] by A29,ZFMISC_1:def 2; reconsider y, z as Point of T2 by A31,A32; set r3 = z`1-o`1, r4 = z`2-o`2; A34: Zf1. [y,z] = f1. [y,z] by A4,A5,A11,A31,A32; A35: Zxo. [y,z] = xo. [y,z] by A4,A5,A12,A31,A32; A36: Zyo. [y,z] = yo. [y,z] by A4,A5,A13,A31,A32; A37: xo. [y,z] = [y,z]`2`1 - o`1 by Def1; A38: yo. [y,z] = [y,z]`2`2 - o`2 by Def2; dom p2 c= the carrier of TD by RELAT_1:def 18; then A39: a in the carrier of TD by A29; A40: p2. [y,z] = (Zxo(#)Zxo + Zyo(#)Zyo). [y,z] - Zf1. [y,z] by A29,A33,VALUED_1:13 .= (Zxo(#)Zxo + Zyo(#)Zyo). [y,z] - r^2 by A34,FUNCOP_1:7 .= (Zxo(#)Zxo). [y,z] + (Zyo(#)Zyo). [y,z] - r^2 by A33,A39,VALUED_1:1 .= Zxo. [y,z] * Zxo. [y,z] + (Zyo(#)Zyo). [y,z] - r^2 by VALUED_1:5 .= r3^2+r4^2-r^2 by A35,A36,A37,A38,VALUED_1:5; z = p by A32,TARSKI:def 1; then |. z-o .| <= r by A1,A3,TOPREAL9:8; then A41: |. z-o .|^2 <= r^2 by SQUARE_1:15; |. z-o .|^2 = ((z-o)`1)^2+((z-o)`2)^2 by JGRAPH_1:29 .= r3^2+((z-o)`2)^2 by TOPREAL3:3 .= r3^2+r4^2 by TOPREAL3:3; then r3^2+r4^2-r^2 <= r^2-r^2 by A41,XREAL_1:9; hence 0 >= b by A30,A33,A40; end; then reconsider p2 as nonpositive-yielding continuous RealMap of TD by PARTFUN3:def 3; set pp = p1 - m(#)p2; set k = (-(xx+yy) + sqrt(pp)) / m; set x3 = Zfx2 + k(#)Zdx; set y3 = Zfy2 + k(#)Zdy; reconsider X3 = x3, Y3 = y3 as Function of TD,R^1 by TOPMETR:17; set F = <:X3,Y3:>; set R = R2Homeomorphism; A42: for x being Point of D1 holds gg.x = (R*F). [x,p] proof let x be Point of D1; consider y being Point of T2 such that A43: x = y and A44: gg.x = HC(p,y,o,r) by A1,Def7; A45: x <> p by A4,ZFMISC_1:56; A46: [y,p] in OK by A2,A4,A43,ZFMISC_1:def 2; set r1 = y`1-p`1, r2 = y`2-p`2, r3 = p`1-o`1, r4 = p`2-o`2; set l = (-(r3*r1+r4*r2)+sqrt((r3*r1+r4*r2)^2-(r1^2+r2^2)*(r3^2+r4^2-r^2))) / (r1^2+r2^2); A47: fx2. [y,p] = [y,p]`2`1 by Def5; A48: fy2. [y,p] = [y,p]`2`2 by Def6; A49: dx. [y,p] = [y,p]`1`1 - [y,p]`2`1 by Def3; A50: dy. [y,p] = [y,p]`1`2 - [y,p]`2`2 by Def4; A51: xo. [y,p] = [y,p]`2`1 - o`1 by Def1; A52: yo. [y,p] = [y,p]`2`2 - o`2 by Def2; A53: dom X3 = the carrier of TD by FUNCT_2:def 1; A54: dom Y3 = the carrier of TD by FUNCT_2:def 1; A55: dom pp = the carrier of TD by FUNCT_2:def 1; A56: p is Point of D2 by A5,TARSKI:def 1; then A57: Zdx. [y,p] = dx. [y,p] by A7,A43; A58: Zdy. [y,p] = dy. [y,p] by A8,A43,A56; A59: Zf1. [y,p] = f1. [y,p] by A11,A43,A56; A60: Zxo. [y,p] = xo. [y,p] by A12,A43,A56; A61: Zyo. [y,p] = yo. [y,p] by A13,A43,A56; A62: m. [y,p] = (Zdx(#)Zdx). [y,p] + (Zdy(#)Zdy). [y,p] by A6,A46,VALUED_1:1 .= Zdx. [y,p] * Zdx. [y,p] + (Zdy(#)Zdy). [y,p] by VALUED_1:5 .= r1^2+r2^2 by A49,A50,A57,A58,VALUED_1:5; A63: xx. [y,p] = Zxo. [y,p] * Zdx. [y,p] by VALUED_1:5; A64: yy. [y,p] = Zyo. [y,p] * Zdy. [y,p] by VALUED_1:5; A65: (xx+yy). [y,p] = xx. [y,p] + yy. [y,p] by A6,A46,VALUED_1:1; then A66: p1. [y,p] = (r3*r1+r4*r2)^2 by A49,A50,A51,A52,A57,A58,A60,A61,A63,A64,VALUED_1:5; A67: p2. [y,p] = (Zxo(#)Zxo + Zyo(#)Zyo). [y,p] - Zf1. [y,p] by A6,A28,A46,VALUED_1:13 .= (Zxo(#)Zxo + Zyo(#)Zyo). [y,p] - r^2 by A59,FUNCOP_1:7 .= (Zxo(#)Zxo). [y,p] + (Zyo(#)Zyo). [y,p] - r^2 by A6,A46,VALUED_1:1 .= Zxo. [y,p] * Zxo. [y,p] + (Zyo(#)Zyo). [y,p] - r^2 by VALUED_1:5 .= r3^2+r4^2-r^2 by A51,A52,A60,A61,VALUED_1:5; dom sqrt pp = the carrier of TD by FUNCT_2:def 1; then A68: sqrt(pp). [y,p] = sqrt(pp. [y,p]) by A6,A46,PARTFUN3:def 5 .= sqrt(p1. [y,p] - (m(#)p2). [y,p]) by A6,A46,A55,VALUED_1:13 .= sqrt((r3*r1+r4*r2)^2-(r1^2+r2^2)*(r3^2+r4^2-r^2)) by A62,A66,A67,VALUED_1:5; dom k = the carrier of TD by FUNCT_2:def 1; then A69: k. [y,p] = (-(xx+yy) + sqrt(pp)). [y,p] * (m. [y,p])" by A6,A46, RFUNCT_1:def 1 .= (-(xx+yy) + sqrt(pp)). [y,p] / m. [y,p] by XCMPLX_0:def 9 .= ((-(xx+yy)). [y,p] + sqrt(pp). [y,p]) / (r1^2+r2^2) by A6,A46,A62,VALUED_1:1 .= l by A49,A50,A51,A52,A57,A58,A60,A61,A63,A64,A65,A68,VALUED_1:8; A70: X3. [y,p] = Zfx2. [y,p] + (k(#)Zdx). [y,p] by A6,A46,VALUED_1:1 .= p`1 + (k(#)Zdx). [y,p] by A9,A43,A47,A56 .= p`1+l*r1 by A49,A57,A69,VALUED_1:5; A71: Y3. [y,p] = Zfy2. [y,p] + (k(#)Zdy). [y,p] by A6,A46,VALUED_1:1 .= p`2 + (k(#)Zdy). [y,p] by A10,A43,A48,A56 .= p`2+l*r2 by A50,A58,A69,VALUED_1:5; A72: y in Bp by A4,A43; Bp c= cB by XBOOLE_1:36; hence gg.x = |[ p`1+l*r1, p`2+l*r2 ]| by A1,A3,A43,A44,A45,A72,BROUWER:8 .= R. [X3. [y,p], Y3. [y,p]] by A70,A71,TOPREALA:def 2 .= R.(F. [y,p]) by A6,A46,A53,A54,FUNCT_3:49 .= (R*F). [x,p] by A6,A43,A46,FUNCT_2:15; end; A73: X3 is continuous by JORDAN5A:27; Y3 is continuous by JORDAN5A:27; then reconsider F as continuous Function of TD,[:R^1,R^1:] by A73,YELLOW12:41; for pp being Point of D1, V being Subset of S1 st gg.pp in V & V is open holds ex W being Subset of D1 st pp in W & W is open & gg.:W c= V proof let pp be Point of D1, V be Subset of S1 such that A74: gg.pp in V and A75: V is open; reconsider p1 = pp, fp = p as Point of T2 by PRE_TOPC:25; A76: [pp,p] in OK by A2,A4,ZFMISC_1:def 2; consider V1 being Subset of T2 such that A77: V1 is open and A78: V1 /\ [#]S1 = V by A75,TOPS_2:24; A79: gg.pp = (R*F). [pp,p] by A42; R" is being_homeomorphism by TOPREALA:34,TOPS_2:56; then A80: R" .:V1 is open by A77,TOPGRP_1:25; A81: dom F = the carrier of [:T2,T2:] | OK by FUNCT_2:def 1; A82: dom R = the carrier of [:R^1,R^1:] by FUNCT_2:def 1; then A83: rng F c= dom R; then A84: dom (R*F) = dom F by RELAT_1:27; A85: rng R = [#]T2 by TOPREALA:34,TOPS_2:def 5; A86: R"*(R*F) = R"*R*F by RELAT_1:36 .= id dom R*F by A85,TOPREALA:34,TOPS_2:52; dom id dom R = dom R; then A87: dom (id dom R*F) = dom F by A83,RELAT_1:27; for x being object st x in dom F holds (id dom R*F).x = F.x proof let x be object such that A88: x in dom F; A89: F.x in rng F by A88,FUNCT_1:def 3; thus (id dom R*F).x = id dom R.(F.x) by A88,FUNCT_1:13 .= F.x by A82,A89,FUNCT_1:18; end; then A90: id dom R*F = F by A87,FUNCT_1:2; (R*F). [p1,fp] in V1 by A74,A78,A79,XBOOLE_0:def 4; then R" .((R*F). [p1,fp]) in R" .:V1 by FUNCT_2:35; then (R"*(R*F)). [p1,fp] in R" .:V1 by A6,A76,A81,A84,FUNCT_1:13; then consider W being Subset of TD such that A91: [p1,fp] in W and A92: W is open and A93: F.:W c= R" .:V1 by A6,A76,A80,A86,A90,JGRAPH_2:10; consider WW being Subset of [:T2,T2:] such that A94: WW is open and A95: WW /\ [#]TD = W by A92,TOPS_2:24; consider SF being Subset-Family of [:T2,T2:] such that A96: WW = union SF and A97: for e being set st e in SF ex X1 being Subset of T2, Y1 being Subset of T2 st e = [:X1,Y1:] & X1 is open & Y1 is open by A94,BORSUK_1:5; [p1,fp] in WW by A91,A95,XBOOLE_0:def 4; then consider Z being set such that A98: [p1,fp] in Z and A99: Z in SF by A96,TARSKI:def 4; consider X1, Y1 being Subset of T2 such that A100: Z = [:X1,Y1:] and A101: X1 is open and Y1 is open by A97,A99; set ZZ = Z /\ [#]TD; reconsider XX = X1 /\ [#]D1 as open Subset of D1 by A101,TOPS_2:24; take XX; pp in X1 by A98,A100,ZFMISC_1:87; hence pp in XX by XBOOLE_0:def 4; thus XX is open; let b be object; assume b in gg.:XX; then consider a being Point of D1 such that A102: a in XX and A103: b = gg.a by FUNCT_2:65; reconsider a1 = a, fa = fp as Point of T2 by PRE_TOPC:25; A104: a in X1 by A102,XBOOLE_0:def 4; A105: [a,p] in OK by A2,A4,ZFMISC_1:def 2; fa in Y1 by A98,A100,ZFMISC_1:87; then [a,fa] in Z by A100,A104,ZFMISC_1:def 2; then [a,fa] in ZZ by A6,A105,XBOOLE_0:def 4; then A106: F. [a1,fa] in F.:ZZ by FUNCT_2:35; A107: R qua Function" = R" by TOPREALA:34,TOPS_2:def 4; A108: dom(R") = [#]T2 by A85,TOPREALA:34,TOPS_2:49; Z c= WW by A96,A99,ZFMISC_1:74; then ZZ c= WW /\ [#]TD by XBOOLE_1:27; then F.:ZZ c= F.:W by A95,RELAT_1:123; then F. [a1,fa] in F.:W by A106; then R.(F. [a1,fa]) in R.:(R" .:V1) by A93,FUNCT_2:35; then (R*F). [a1,fa] in R.:(R" .:V1) by A6,A105,FUNCT_2:15; then (R*F). [a1,fa] in V1 by A107,A108,PARTFUN3:1,TOPREALA:34; then gg.a in V1 by A42; hence thesis by A78,A103,XBOOLE_0:def 4; end; hence thesis by JGRAPH_2:10; end; theorem Th65: for n being non zero Element of NAT, o, p being Point of TOP-REAL n, r being positive Real st p in Ball(o,r) holds DiskProj(o,r,p)|Sphere(o,r) = id Sphere(o,r) proof let n be non zero Element of NAT; let o, p be Point of TOP-REAL n; let r be positive Real; assume A1: p in Ball(o,r); A2: the carrier of Tdisk(o,r) = cl_Ball(o,r) by BROUWER:3; A3: the carrier of (TOP-REAL n)|(cl_Ball(o,r)\{p}) = cl_Ball(o,r)\{p} by PRE_TOPC:8; A4: dom DiskProj(o,r,p) = the carrier of (TOP-REAL n)|(cl_Ball(o,r)\{p}) by FUNCT_2:def 1; A5: Sphere(o,r) misses Ball(o,r) by TOPREAL9:19; A6: Sphere(o,r) c= cl_Ball(o,r) by TOPREAL9:17; A7: Ball(o,r) c= cl_Ball(o,r) by TOPREAL9:16; A8: Sphere(o,r) c= cl_Ball(o,r)\{p} proof let a be object; assume A9: a in Sphere(o,r); then a <> p by A1,A5,XBOOLE_0:3; hence thesis by A6,A9,ZFMISC_1:56; end; then A10: dom(DiskProj(o,r,p)|Sphere(o,r)) = Sphere(o,r) by A3,A4,RELAT_1:62; A11: dom id Sphere(o,r) = Sphere(o,r); now let x be object; assume A12: x in dom(DiskProj(o,r,p)|Sphere(o,r)); then x in dom DiskProj(o,r,p) by RELAT_1:57; then consider y being Point of TOP-REAL n such that A13: x = y and A14: (DiskProj(o,r,p)).x = HC(p,y,o,r) by A1,A2,A7,Def7; y in halfline(p,y) by TOPREAL9:28; then A15: x in halfline(p,y) /\ Sphere(o,r) by A12,A13,XBOOLE_0:def 4; A16: x <> p by A1,A5,A12,XBOOLE_0:3; thus (DiskProj(o,r,p)|Sphere(o,r)).x = (DiskProj(o,r,p)).x by A12,FUNCT_1:47 .= x by A1,A2,A6,A7,A10,A12,A13,A14,A15,A16,BROUWER:def 3 .= (id Sphere(o,r)).x by A12,FUNCT_1:18; end; hence thesis by A3,A4,A8,A11,FUNCT_1:2,RELAT_1:62; end; definition let n be non zero Element of NAT, o, p be Point of TOP-REAL n, r be positive Real such that A1: p in Ball(o,r); set X = Tcircle(o,r); func RotateCircle(o,r,p) -> Function of Tcircle(o,r), Tcircle(o,r) means :Def8: for x being Point of Tcircle(o,r) ex y being Point of TOP-REAL n st x = y & it.x = HC(y,p,o,r); existence proof A2: the carrier of X = Sphere(o,r) by TOPREALB:9; defpred P[object,object] means ex z being Point of TOP-REAL n st $1 = z & $2 = HC(z,p,o,r); A3: for x being object st x in the carrier of X ex y being object st y in the carrier of X & P[x,y] proof let x be object such that A4: x in the carrier of X; reconsider z = x as Point of TOP-REAL n by A4,PRE_TOPC:25; Sphere(o,r) c= cl_Ball(o,r) by TOPREAL9:17; then A5: z is Point of Tdisk(o,r) by A2,A4,BROUWER:3; Ball(o,r) c= cl_Ball(o,r) by TOPREAL9:16; then A6: p is Point of Tdisk(o,r) by A1,BROUWER:3; Ball(o,r) misses Sphere(o,r) by TOPREAL9:19; then p <> z by A1,A2,A4,XBOOLE_0:3; then HC(z,p,o,r) is Point of X by A5,A6,BROUWER:6; hence thesis; end; consider f being Function of the carrier of X, the carrier of X such that A7: for x being object st x in the carrier of X holds P[x,f.x] from FUNCT_2:sch 1(A3); reconsider f as Function of X, X; take f; let x be Point of X; thus thesis by A7; end; uniqueness proof let f, g be Function of X, X such that A8: for x being Point of X ex y being Point of TOP-REAL n st x = y & f.x = HC(y,p,o,r) and A9: for x being Point of X ex y being Point of TOP-REAL n st x = y & g.x = HC(y,p,o,r); now let x be object such that A10: x in the carrier of X; A11: ex y being Point of TOP-REAL n st x = y & f.x = HC(y,p,o,r) by A8,A10; ex y being Point of TOP-REAL n st x = y & g.x = HC(y,p,o,r) by A9,A10; hence f.x = g.x by A11; end; hence thesis by FUNCT_2:12; end; end; theorem Th66: for o, p being Point of TOP-REAL 2, r being positive Real st p in Ball(o,r) holds RotateCircle(o,r,p) is continuous proof let o, p be Point of TOP-REAL 2; let r be positive Real such that A1: p in Ball(o,r); set D = Tdisk(o,r); set cB = cl_Ball(o,r); set Bp = Sphere(o,r); set OK = [:{p},Bp:]; set D1 = T2|{p}; set D2 = T2|Bp; set S1 = Tcircle(o,r); A2: D2 = S1 by TOPREALB:def 6; A3: Ball(o,r) misses Sphere(o,r) by TOPREAL9:19; A4: p in {p} by TARSKI:def 1; A5: Bp c= cB by TOPREAL9:17; A6: Ball(o,r) c= cB by TOPREAL9:16; A7: the carrier of D = cB by BROUWER:3; A8: the carrier of D1 = {p} by PRE_TOPC:8; A9: the carrier of D2 = Bp by PRE_TOPC:8; set TD = [:T2,T2:] | OK; set gg = RotateCircle(o,r,p); set xo = diffX2_1(o); set yo = diffX2_2(o); set dx = diffX1_X2_1; set dy = diffX1_X2_2; set fx2 = Proj2_1; set fy2 = Proj2_2; reconsider rr = r^2 as Element of REAL by XREAL_0:def 1; set f1 = (the carrier of [:T2,T2:]) --> rr; reconsider f1 as continuous RealMap of [:T2,T2:] by Lm6; set Zf1 = f1 | OK; set Zfx2 = fx2 | OK; set Zfy2 = fy2 | OK; set Zdx = dx | OK; set Zdy = dy | OK; set Zxo = xo | OK; set Zyo = yo | OK; set xx = Zxo(#)Zdx; set yy = Zyo(#)Zdy; set m = Zdx(#)Zdx + Zdy(#)Zdy; A10: the carrier of TD = OK by PRE_TOPC:8; A11: for y being Point of D1, z being Point of D2 holds Zdx. [y,z] = dx. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A8,A9,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; A12: for y being Point of D1, z being Point of D2 holds Zdy. [y,z] = dy. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A8,A9,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; A13: for y being Point of D1, z being Point of D2 holds Zfx2. [y,z] = fx2. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A8,A9,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; A14: for y being Point of D1, z being Point of D2 holds Zfy2. [y,z] = fy2. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A8,A9,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; A15: for y being Point of D1, z being Point of D2 holds Zf1. [y,z] = f1. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A8,A9,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; A16: for y being Point of D1, z being Point of D2 holds Zxo. [y,z] = xo. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A8,A9,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; A17: for y being Point of D1, z being Point of D2 holds Zyo. [y,z] = yo. [y,z] proof let y be Point of D1; let z be Point of D2; [y,z] in OK by A8,A9,ZFMISC_1:def 2; hence thesis by FUNCT_1:49; end; now let b be Real; assume b in rng m; then consider a being object such that A18: a in dom m and A19: m.a = b by FUNCT_1:def 3; consider y, z being object such that A20: y in {p} and A21: z in Bp and A22: a = [y,z] by A18,ZFMISC_1:def 2; A23: y = p by A20,TARSKI:def 1; reconsider y, z as Point of T2 by A20,A21; A24: y <> z by A1,A3,A21,A23,XBOOLE_0:3; A25: dx. [y,z] = [y,z]`1`1 - [y,z]`2`1 by Def3; A26: dy. [y,z] = [y,z]`1`2 - [y,z]`2`2 by Def4; set r1 = y`1-z`1; set r2 = y`2-z`2; A27: Zdx. [y,z] = dx. [y,z] by A8,A9,A11,A20,A21; A28: Zdy. [y,z] = dy. [y,z] by A8,A9,A12,A20,A21; dom m c= the carrier of TD by RELAT_1:def 18; then a in the carrier of TD by A18; then A29: m. [y,z] = (Zdx(#)Zdx). [y,z] + (Zdy(#)Zdy). [y,z] by A22,VALUED_1:1 .= Zdx. [y,z] * Zdx. [y,z] + (Zdy(#)Zdy). [y,z] by VALUED_1:5 .= r1^2+r2^2 by A25,A26,A27,A28,VALUED_1:5; now assume A30: r1^2+r2^2 = 0; then A31: r1 = 0 by COMPLEX1:1; r2 = 0 by A30,COMPLEX1:1; hence contradiction by A24,A31,TOPREAL3:6; end; hence 0 < b by A19,A22,A29; end; then reconsider m as positive-yielding continuous RealMap of TD by PARTFUN3:def 1; set p1 = (xx+yy)(#)(xx+yy); set p2 = Zxo(#)Zxo + Zyo(#)Zyo - Zf1; A32: dom p2 = the carrier of TD by FUNCT_2:def 1; now let b be Real; assume b in rng p2; then consider a being object such that A33: a in dom p2 and A34: p2.a = b by FUNCT_1:def 3; consider y, z being object such that A35: y in {p} and A36: z in Bp and A37: a = [y,z] by A33,ZFMISC_1:def 2; reconsider y, z as Point of T2 by A35,A36; set r3 = z`1-o`1, r4 = z`2-o`2; A38: Zf1. [y,z] = f1. [y,z] by A8,A9,A15,A35,A36; A39: Zxo. [y,z] = xo. [y,z] by A8,A9,A16,A35,A36; A40: Zyo. [y,z] = yo. [y,z] by A8,A9,A17,A35,A36; A41: xo. [y,z] = [y,z]`2`1 - o`1 by Def1; A42: yo. [y,z] = [y,z]`2`2 - o`2 by Def2; dom p2 c= the carrier of TD by RELAT_1:def 18; then A43: a in the carrier of TD by A33; A44: p2. [y,z] = (Zxo(#)Zxo + Zyo(#)Zyo). [y,z] - Zf1. [y,z] by A33,A37,VALUED_1:13 .= (Zxo(#)Zxo + Zyo(#)Zyo). [y,z] - r^2 by A38,FUNCOP_1:7 .= (Zxo(#)Zxo). [y,z] + (Zyo(#)Zyo). [y,z] - r^2 by A37,A43,VALUED_1:1 .= Zxo. [y,z] * Zxo. [y,z] + (Zyo(#)Zyo). [y,z] - r^2 by VALUED_1:5 .= r3^2+r4^2-r^2 by A39,A40,A41,A42,VALUED_1:5; |. z-o .| <= r by A5,A36,TOPREAL9:8; then A45: |. z-o .|^2 <= r^2 by SQUARE_1:15; |. z-o .|^2 = ((z-o)`1)^2+((z-o)`2)^2 by JGRAPH_1:29 .= r3^2+((z-o)`2)^2 by TOPREAL3:3 .= r3^2+r4^2 by TOPREAL3:3; then r3^2+r4^2-r^2 <= r^2-r^2 by A45,XREAL_1:9; hence 0 >= b by A34,A37,A44; end; then reconsider p2 as nonpositive-yielding continuous RealMap of TD by PARTFUN3:def 3; set pp = p1 - m(#)p2; set k = (-(xx+yy) + sqrt(pp)) / m; set x3 = Zfx2 + k(#)Zdx; set y3 = Zfy2 + k(#)Zdy; reconsider X3 = x3, Y3 = y3 as Function of TD,R^1 by TOPMETR:17; set F = <:X3,Y3:>; set R = R2Homeomorphism; A46: for x being Point of D2 holds gg.x = (R*F). [p,x] proof let x be Point of D2; consider y being Point of T2 such that A47: x = y and A48: gg.x = HC(y,p,o,r) by A1,A2,Def8; A49: x <> p by A1,A3,A9,XBOOLE_0:3; A50: [p,y] in OK by A4,A9,A47,ZFMISC_1:def 2; set r1 = p`1-y`1, r2 = p`2-y`2, r3 = y`1-o`1, r4 = y`2-o`2; set l = (-(r3*r1+r4*r2)+sqrt((r3*r1+r4*r2)^2-(r1^2+r2^2)*(r3^2+r4^2-r^2))) / (r1^2+r2^2); A51: fx2. [p,y] = [p,y]`2`1 by Def5; A52: fy2. [p,y] = [p,y]`2`2 by Def6; A53: dx. [p,y] = [p,y]`1`1 - [p,y]`2`1 by Def3; A54: dy. [p,y] = [p,y]`1`2 - [p,y]`2`2 by Def4; A55: xo. [p,y] = [p,y]`2`1 - o`1 by Def1; A56: yo. [p,y] = [p,y]`2`2 - o`2 by Def2; A57: dom X3 = the carrier of TD by FUNCT_2:def 1; A58: dom Y3 = the carrier of TD by FUNCT_2:def 1; A59: dom pp = the carrier of TD by FUNCT_2:def 1; A60: p is Point of D1 by A8,TARSKI:def 1; then A61: Zdx. [p,y] = dx. [p,y] by A11,A47; A62: Zdy. [p,y] = dy. [p,y] by A12,A47,A60; A63: Zf1. [p,y] = f1. [p,y] by A15,A47,A60; A64: Zxo. [p,y] = xo. [p,y] by A16,A47,A60; A65: Zyo. [p,y] = yo. [p,y] by A17,A47,A60; A66: m. [p,y] = (Zdx(#)Zdx). [p,y] + (Zdy(#)Zdy). [p,y] by A10,A50,VALUED_1:1 .= Zdx. [p,y] * Zdx. [p,y] + (Zdy(#)Zdy). [p,y] by VALUED_1:5 .= r1^2+r2^2 by A53,A54,A61,A62,VALUED_1:5; A67: xx. [p,y] = Zxo. [p,y] * Zdx. [p,y] by VALUED_1:5; A68: yy. [p,y] = Zyo. [p,y] * Zdy. [p,y] by VALUED_1:5; A69: (xx+yy). [p,y] = xx. [p,y] + yy. [p,y] by A10,A50,VALUED_1:1; then A70: p1. [p,y] = (r3*r1+r4*r2)^2 by A53,A54,A55,A56,A61,A62,A64,A65,A67,A68,VALUED_1:5; A71: p2. [p,y] = (Zxo(#)Zxo + Zyo(#)Zyo). [p,y] - Zf1. [p,y] by A10,A32,A50,VALUED_1:13 .= (Zxo(#)Zxo + Zyo(#)Zyo). [p,y] - r^2 by A63,FUNCOP_1:7 .= (Zxo(#)Zxo). [p,y] + (Zyo(#)Zyo). [p,y] - r^2 by A10,A50,VALUED_1:1 .= Zxo. [p,y] * Zxo. [p,y] + (Zyo(#)Zyo). [p,y] - r^2 by VALUED_1:5 .= r3^2+r4^2-r^2 by A55,A56,A64,A65,VALUED_1:5; dom sqrt pp = the carrier of TD by FUNCT_2:def 1; then A72: sqrt(pp). [p,y] = sqrt(pp. [p,y]) by A10,A50,PARTFUN3:def 5 .= sqrt(p1. [p,y] - (m(#)p2). [p,y]) by A10,A50,A59,VALUED_1:13 .= sqrt((r3*r1+r4*r2)^2-(r1^2+r2^2)*(r3^2+r4^2-r^2)) by A66,A70,A71,VALUED_1:5; dom k = the carrier of TD by FUNCT_2:def 1; then A73: k. [p,y] = (-(xx+yy) + sqrt(pp)). [p,y] * (m. [p,y])" by A10,A50, RFUNCT_1:def 1 .= (-(xx+yy) + sqrt(pp)). [p,y] / m. [p,y] by XCMPLX_0:def 9 .= ((-(xx+yy)). [p,y] + sqrt(pp). [p,y]) / (r1^2+r2^2) by A10,A50,A66,VALUED_1:1 .= l by A53,A54,A55,A56,A61,A62,A64,A65,A67,A68,A69,A72,VALUED_1:8; A74: X3. [p,y] = Zfx2. [p,y] + (k(#)Zdx). [p,y] by A10,A50,VALUED_1:1 .= y`1 + (k(#)Zdx). [p,y] by A13,A47,A51,A60 .= y`1+l*r1 by A53,A61,A73,VALUED_1:5; A75: Y3. [p,y] = Zfy2. [p,y] + (k(#)Zdy). [p,y] by A10,A50,VALUED_1:1 .= y`2 + (k(#)Zdy). [p,y] by A14,A47,A52,A60 .= y`2+l*r2 by A54,A62,A73,VALUED_1:5; y in the carrier of D2 by A47; hence gg.x = |[ y`1+l*r1, y`2+l*r2 ]| by A1,A5,A6,A7,A9,A47,A48,A49, BROUWER:8 .= R. [X3. [p,y], Y3. [p,y]] by A74,A75,TOPREALA:def 2 .= R.(F. [p,y]) by A10,A50,A57,A58,FUNCT_3:49 .= (R*F). [p,x] by A10,A47,A50,FUNCT_2:15; end; A76: X3 is continuous by JORDAN5A:27; Y3 is continuous by JORDAN5A:27; then reconsider F as continuous Function of TD,[:R^1,R^1:] by A76,YELLOW12:41 ; for pp being Point of D2, V being Subset of S1 st gg.pp in V & V is open holds ex W being Subset of D2 st pp in W & W is open & gg.:W c= V proof let pp be Point of D2, V be Subset of S1 such that A77: gg.pp in V and A78: V is open; reconsider p1 = pp, fp = p as Point of T2 by PRE_TOPC:25; A79: [p,pp] in OK by A4,A9,ZFMISC_1:def 2; consider V1 being Subset of T2 such that A80: V1 is open and A81: V1 /\ [#]S1 = V by A78,TOPS_2:24; A82: gg.pp = (R*F). [p,pp] by A46; R" is being_homeomorphism by TOPREALA:34,TOPS_2:56; then A83: R" .:V1 is open by A80,TOPGRP_1:25; A84: dom F = the carrier of [:T2,T2:] | OK by FUNCT_2:def 1; A85: dom R = the carrier of [:R^1,R^1:] by FUNCT_2:def 1; then A86: rng F c= dom R; then A87: dom (R*F) = dom F by RELAT_1:27; A88: rng R = [#]T2 by TOPREALA:34,TOPS_2:def 5; A89: R"*(R*F) = R"*R*F by RELAT_1:36 .= id dom R*F by A88,TOPREALA:34,TOPS_2:52; dom id dom R = dom R; then A90: dom (id dom R*F) = dom F by A86,RELAT_1:27; for x being object st x in dom F holds (id dom R*F).x = F.x proof let x be object such that A91: x in dom F; A92: F.x in rng F by A91,FUNCT_1:def 3; thus (id dom R*F).x = id dom R.(F.x) by A91,FUNCT_1:13 .= F.x by A85,A92,FUNCT_1:18; end; then A93: id dom R*F = F by A90,FUNCT_1:2; (R*F). [fp,p1] in V1 by A77,A81,A82,XBOOLE_0:def 4; then R" .((R*F). [fp,p1]) in R" .:V1 by FUNCT_2:35; then (R"*(R*F)). [fp,p1] in R" .:V1 by A10,A79,A84,A87,FUNCT_1:13; then consider W being Subset of TD such that A94: [fp,p1] in W and A95: W is open and A96: F.:W c= R" .:V1 by A10,A79,A83,A89,A93,JGRAPH_2:10; consider WW being Subset of [:T2,T2:] such that A97: WW is open and A98: WW /\ [#]TD = W by A95,TOPS_2:24; consider SF being Subset-Family of [:T2,T2:] such that A99: WW = union SF and A100: for e being set st e in SF ex X1 being Subset of T2, Y1 being Subset of T2 st e = [:X1,Y1:] & X1 is open & Y1 is open by A97,BORSUK_1:5; [fp,p1] in WW by A94,A98,XBOOLE_0:def 4; then consider Z being set such that A101: [fp,p1] in Z and A102: Z in SF by A99,TARSKI:def 4; consider X1, Y1 being Subset of T2 such that A103: Z = [:X1,Y1:] and X1 is open and A104: Y1 is open by A100,A102; set ZZ = Z /\ [#]TD; reconsider XX = Y1 /\ [#]D2 as open Subset of D2 by A104,TOPS_2:24; take XX; pp in Y1 by A101,A103,ZFMISC_1:87; hence pp in XX by XBOOLE_0:def 4; thus XX is open; let b be object; assume b in gg.:XX; then consider a being Point of D2 such that A105: a in XX and A106: b = gg.a by A2,FUNCT_2:65; reconsider a1 = a, fa = fp as Point of T2 by PRE_TOPC:25; A107: a in Y1 by A105,XBOOLE_0:def 4; A108: [p,a] in OK by A4,A9,ZFMISC_1:def 2; fa in X1 by A101,A103,ZFMISC_1:87; then [fa,a] in Z by A103,A107,ZFMISC_1:def 2; then [fa,a] in ZZ by A10,A108,XBOOLE_0:def 4; then A109: F. [fa,a1] in F.:ZZ by FUNCT_2:35; A110: R qua Function" = R" by TOPREALA:34,TOPS_2:def 4; A111: dom(R") = [#]T2 by A88,TOPREALA:34,TOPS_2:49; A112: gg.a1 in the carrier of S1 by A2,FUNCT_2:5; Z c= WW by A99,A102,ZFMISC_1:74; then ZZ c= WW /\ [#]TD by XBOOLE_1:27; then F.:ZZ c= F.:W by A98,RELAT_1:123; then F. [fa,a1] in F.:W by A109; then R.(F. [fa,a1]) in R.:(R" .:V1) by A96,FUNCT_2:35; then (R*F). [fa,a1] in R.:(R" .:V1) by A10,A108,FUNCT_2:15; then (R*F). [fa,a1] in V1 by A110,A111,PARTFUN3:1,TOPREALA:34; then gg.a in V1 by A46; hence thesis by A81,A106,A112,XBOOLE_0:def 4; end; hence thesis by A2,JGRAPH_2:10; end; theorem Th67: for n being non zero Element of NAT for o, p being Point of TOP-REAL n, r being positive Real st p in Ball(o,r) holds RotateCircle(o,r,p) is without_fixpoints proof let n be non zero Element of NAT; let o, p be Point of TOP-REAL n; let r be positive Real; assume A1: p in Ball(o,r); set f = RotateCircle(o,r,p); let x be object; assume A2: x in dom f; set S = Tcircle(o,r); A3: dom f = the carrier of S by FUNCT_2:def 1; consider y being Point of TOP-REAL n such that A4: x = y and A5: f.x = HC(y,p,o,r) by A1,A2,Def8; A6: the carrier of S = Sphere(o,r) by TOPREALB:9; Sphere(o,r) c= cl_Ball(o,r) by TOPREAL9:17; then A7: y is Point of Tdisk(o,r) by A2,A3,A4,A6,BROUWER:3; Ball(o,r) c= cl_Ball(o,r) by TOPREAL9:16; then A8: p is Point of Tdisk(o,r) by A1,BROUWER:3; Ball(o,r) misses Sphere(o,r) by TOPREAL9:19; then y <> p by A1,A2,A4,A6,XBOOLE_0:3; hence thesis by A4,A5,A7,A8,BROUWER:def 3; end; begin :: Jordan's Curve Theorem theorem Th68: U = P & U is a_component & V is a_component & U <> V implies Cl P misses V proof assume that A1: U = P and A2: U is a_component and A3: V is a_component and A4: U <> V; assume Cl P meets V; then A5: ex x being object st x in Cl P & x in V by XBOOLE_0:3; the carrier of T2|C` = C` by PRE_TOPC:8; then reconsider V1 = V as Subset of T2 by XBOOLE_1:1; reconsider T2C = T2|C` as non empty SubSpace of T2; T2C is locally_connected by JORDAN2C:81; then V is open by A3,CONNSP_2:15; then V1 is open by TSEP_1:17; then P meets V1 by A5,PRE_TOPC:def 7; hence thesis by A1,A2,A3,A4,CONNSP_1:35; end; theorem Th69: U is a_component implies (TOP-REAL 2)|C`|U is pathwise_connected proof set T = T2|C`; assume A1: U is a_component; let a, b be Point of T|U; A2: the carrier of T|U = U by PRE_TOPC:8; A3: U <> {}T by A1,CONNSP_1:32; per cases; suppose A4: a = b; reconsider TU = T|U as non empty TopSpace by A3; reconsider a as Point of TU; reconsider f = I[01] --> a as Function of I[01],T|U; take f; thus thesis by A4,BORSUK_1:def 14,def 15,TOPALG_3:4; end; suppose A5: a <> b; A6: T|U is SubSpace of T2 by TSEP_1:7; then reconsider a1 = a, b1 = b as Point of T2 by A3,PRE_TOPC:25; reconsider V = U as Subset of T2 by PRE_TOPC:11; V is_a_component_of C` by A1; then A7: V is open by SPRECT_3:8; U is connected by A1; then V is connected by CONNSP_1:23; then consider P being Subset of T2 such that A8: P is_S-P_arc_joining a1,b1 and A9: P c= V by A2,A3,A5,A7,TOPREAL4:29; A10: a1 in P by A8,TOPREAL4:3; P is_an_arc_of a1,b1 by A8,TOPREAL4:2; then consider g being Function of I[01], T2|P such that A11: g is being_homeomorphism and A12: g.0 = a and A13: g.1 = b by TOPREAL1:def 1; A14: the carrier of T2|P = P by PRE_TOPC:8; then reconsider f = g as Function of I[01], T|U by A2,A9,A10,FUNCT_2:7; take f; T2|P is SubSpace of T|U by A2,A6,A9,A14,TSEP_1:4; hence f is continuous by A11,PRE_TOPC:26; thus thesis by A12,A13; end; end; ::Th5_6: ex r ... Lm12: for r being non negative Real st A is_an_arc_of p1,p2 & A is Subset of Tdisk(p,r) ex f being Function of Tdisk(p,r), (TOP-REAL 2)|A st f is continuous & f|A = id A proof let r be non negative Real; set D = Tdisk(p,r); assume that A1: A is_an_arc_of p1,p2 and A2: A is Subset of D; reconsider A1 = A as non empty Subset of D by A1,A2,TOPREAL1:1; reconsider A2 = A as non empty Subset of T2 by A1,TOPREAL1:1; set TA = T2|A2; consider h being Function of I[01],TA such that A3: h is being_homeomorphism and h.0 = p1 and h.1 = p2 by A1,TOPREAL1:def 1; A4: h1 is being_homeomorphism by TREAL_1:17; reconsider hh = h as Function of C0,TA by TOPMETR:20; A5: TA = D|A1 by TOPALG_5:4; then reconsider f = h1*hh" as Function of D|A1,C1; A is closed by A1,JORDAN6:11; then A6: A1 is closed by TSEP_1:12; hh" is continuous by A3,TOPMETR:20,TOPS_2:def 5; then consider g being continuous Function of D,C1 such that A7: g|A1 = f by A4,A5,A6,TIETZE:23; reconsider R = hh*h1"*g as Function of D,(TOP-REAL 2)|A; take R; h1" is continuous by A4,TOPS_2:def 5; hence R is continuous by A3,TOPMETR:20; A8: the carrier of TA = A1 by PRE_TOPC:8; A9: dom R = the carrier of D by FUNCT_2:def 1; A10: dom id A = A; now let a be object; assume A11: a in dom(R|A); then A12: a in dom R by RELAT_1:57; A13: dom g = the carrier of D by FUNCT_2:def 1; A14: dom(h1*hh") = the carrier of TA by FUNCT_2:def 1; A15: hh*h1"*(h1*hh") = hh*h1"*h1*hh" by RELAT_1:36 .= hh*(h1"*h1)*hh" by RELAT_1:36 .= hh*id C0*hh" by A4,GRCAT_1:41 .= hh*hh" by FUNCT_2:17 .= id TA by A3,GRCAT_1:41; thus (R|A).a = R.a by A11,FUNCT_1:49 .= (hh*h1").(g.a) by A13,A12,FUNCT_1:13 .= (hh*h1").((h1*hh").a) by A7,A11,FUNCT_1:49 .= (id A).a by A8,A11,A14,A15,FUNCT_1:13; end; hence thesis by A2,A9,A10,FUNCT_1:2,RELAT_1:62; end; ::Th5_6: ex f ... Lm13: for r being positive Real st A is_an_arc_of p1,p2 & A c= C & C c= Ball(p,r) & p in U & Cl P /\ P` c= A & P c= Ball(p,r) for f being Function of Tdisk(p,r), (TOP-REAL 2)|A st f is continuous & f|A = id A & :: komponenty U = P & U is a_component & B = cl_Ball(p,r) \ {p} ex g being Function of Tdisk(p,r), (TOP-REAL 2)|B st g is continuous & for x being Point of Tdisk(p,r) holds (x in Cl P implies g.x = f.x) & (x in P` implies g.x = x) proof let r be positive Real; set D = Tdisk(p,r); assume that A1: A is_an_arc_of p1,p2 and A2: A c= C and A3: C c= Ball(p,r) and A4: p in U and A5: Cl P /\ P` c= A and A6: P c= Ball(p,r); let f be Function of D, T2|A; assume that A7: f is continuous and A8: f|A = id A and A9: U = P and A10: U is a_component and A11: B = cl_Ball(p,r) \ {p}; reconsider B1 = B as non empty Subset of T2 by A11; reconsider T2B1 = T2|B1 as non empty SubSpace of T2; A12: the carrier of T2|C` = C` by PRE_TOPC:8; A13: the carrier of T2|A = A by PRE_TOPC:8; A14: the carrier of D = cl_Ball(p,r) by BROUWER:3; A15: Ball(p,r) c= cl_Ball(p,r) by TOPREAL9:16; A16: A <> {} by A1,TOPREAL1:1; reconsider A1 = A as non empty Subset of T2 by A1,TOPREAL1:1; A17: not p in C by A4,A12,XBOOLE_0:def 5; |. p-p .| = 0 by TOPRNS_1:28; then A18: p in [#]D by A14,TOPREAL9:8; A19: P c= Cl P by PRE_TOPC:18; then reconsider F1 = (Cl P) /\ [#]D as non empty Subset of D by A4,A9,A18,XBOOLE_0:def 4; A20: Sphere(p,r) c= cl_Ball(p,r) by TOPREAL9:17; A21: Ball(p,r) misses Sphere(p,r) by TOPREAL9:19; consider e being Point of T2 such that A22: e in Sphere(p,r) by SUBSET_1:4; not e in P by A6,A21,A22,XBOOLE_0:3; then e in P` by SUBSET_1:29; then reconsider F3 = P` /\ [#]D as non empty Subset of D by A14,A20,A22,XBOOLE_0:def 4; reconsider T1 = D|F1 as non empty SubSpace of D; reconsider T3 = D|F3 as non empty SubSpace of D; A23: the carrier of T1 = F1 by PRE_TOPC:8; A24: the carrier of T3 = F3 by PRE_TOPC:8; A25: the carrier of T2B1 = B1 by PRE_TOPC:8; A26: A c= B proof let a be object; assume a in A; then A27: a in C by A2; then a in Ball(p,r) by A3; hence thesis by A11,A15,A17,A27,ZFMISC_1:56; end; A28: F3 c= B proof let a be object; assume A29: a in F3; then a in P` by XBOOLE_0:def 4; then not a in P by XBOOLE_0:def 5; hence thesis by A4,A9,A11,A14,A29,ZFMISC_1:56; end; f|F1 is Function of F1,A by A13,A16,FUNCT_2:32; then reconsider f1 = f|F1 as Function of T1,T2B1 by A16,A23,A25,A26,FUNCT_2:7; reconsider g1 = id F3 as Function of T3,T2B1 by A24,A25,A28,FUNCT_2:7; A30: F1 = [#]T1 by PRE_TOPC:8; A31: F3 = [#]T3 by PRE_TOPC:8; A32: [#]T1 \/ [#]T3 = [#]D proof thus [#]T1 \/ [#]T3 c= [#]D by A30,A31,XBOOLE_1:8; let p be object; assume A33: p in [#]D; per cases; suppose p in P; then p in F1 by A19,A33,XBOOLE_0:def 4; hence thesis by A30,XBOOLE_0:def 3; end; suppose not p in P; then p in P` by A14,A33,SUBSET_1:29; then p in F3 by A33,XBOOLE_0:def 4; hence thesis by A31,XBOOLE_0:def 3; end; end; reconsider DT = [#]D as closed Subset of T2 by BORSUK_1:def 11,TSEP_1:1; DT /\ Cl P is closed; then A34: F1 is closed by TSEP_1:8; P is_a_component_of C` by A9,A10; then P is open by SPRECT_3:8; then DT /\ P` is closed; then A35: F3 is closed by TSEP_1:8; reconsider f2 = f|F1 as Function of T1,T2|A1 by A23,FUNCT_2:32; A36: T2|A1 is SubSpace of T2B1 by A13,A25,A26,TSEP_1:4; T3 is SubSpace of T2 by TSEP_1:7; then A37: T3 is SubSpace of T2B1 by A24,A25,A28,TSEP_1:4; f2 is continuous by A7,TOPMETR:7; then A38: f1 is continuous by A36,PRE_TOPC:26; reconsider g2 = id F3 as Function of T3,T3 by A24; g2 = id T3 by PRE_TOPC:8; then A39: g1 is continuous by A37,PRE_TOPC:26; A40: for x being set st x in Cl P & x in P` holds f.x = x proof let x be set; assume that A41: x in Cl P and A42: x in P`; A43: x in Cl P /\ P` by A41,A42,XBOOLE_0:def 4; then (id A).x = x by A5,FUNCT_1:18; hence thesis by A5,A8,A43,FUNCT_1:49; end; for x being object st x in [#]T1 /\ [#]T3 holds f1.x = g1.x proof let x be object; assume A44: x in [#]T1 /\ [#]T3; then A45: x in [#]T1 by XBOOLE_0:def 4; then A46: x in Cl P by A30,XBOOLE_0:def 4; x in P` by A31,A44,XBOOLE_0:def 4; then A47: f.x = x by A40,A46; thus f1.x = f.x by A30,A45,FUNCT_1:49 .= g1.x by A31,A44,A47,FUNCT_1:18; end; then consider g being Function of D,T2|B such that A48: g = f1+*g1 and A49: g is continuous by A30,A31,A32,A34,A35,A38,A39,JGRAPH_2:1; take g; thus g is continuous by A49; let x be Point of D; A50: dom g1 = the carrier of T3 by FUNCT_2:def 1; hereby assume A51: x in Cl P; then A52: x in F1 by XBOOLE_0:def 4; per cases; suppose not x in dom g1; hence g.x = f1.x by A48,FUNCT_4:11 .= f.x by A52,FUNCT_1:49; end; suppose A53: x in dom g1; then A54: x in P` by XBOOLE_0:def 4; thus g.x = g1.x by A48,A53,FUNCT_4:13 .= x by A53,FUNCT_1:18 .= f.x by A40,A51,A54; end; end; assume x in P`; then A55: x in F3 by XBOOLE_0:def 4; hence g.x = g1.x by A48,A50,FUNCT_4:13 .= x by A55,FUNCT_1:18; end; Lm14: for A being non empty Subset of T2 st U <> V for r being positive Real st A c= C & C c= Ball(p,r) & p in V & Cl P /\ P` c= A & Ball(p,r) meets P for f being Function of Tdisk(p,r), (TOP-REAL 2)|A st f is continuous & f|A = id A & :: komponenty U = P & U is a_component & V is a_component & B = cl_Ball(p,r) \ {p} ex g being Function of Tdisk(p,r), (TOP-REAL 2)|B st g is continuous & for x being Point of Tdisk(p,r) holds (x in Cl P implies g.x = x) & (x in P` implies g.x = f.x) proof let A be non empty Subset of T2 such that A1: U <> V; let r be positive Real; set D = Tdisk(p,r); assume that A2: A c= C and A3: C c= Ball(p,r) and A4: p in V and A5: Cl P /\ P` c= A and A6: Ball(p,r) meets P; let f be Function of D, T2|A; assume that A7: f is continuous and A8: f|A = id A and A9: U = P and A10: U is a_component and A11: V is a_component and A12: B = cl_Ball(p,r) \ {p}; reconsider B1 = B as non empty Subset of T2 by A12; reconsider T2B1 = T2|B1 as non empty SubSpace of T2; A13: the carrier of T2|C` = C` by PRE_TOPC:8; A14: the carrier of T2|A = A by PRE_TOPC:8; A15: the carrier of D = cl_Ball(p,r) by BROUWER:3; A16: Ball(p,r) c= cl_Ball(p,r) by TOPREAL9:16; A17: not p in C by A4,A13,XBOOLE_0:def 5; |. p-p .| = 0 by TOPRNS_1:28; then A18: p in [#]D by A15,TOPREAL9:8; A19: P c= Cl P by PRE_TOPC:18; ex j being object st j in Ball(p,r) & j in P by A6,XBOOLE_0:3; then reconsider F1 = (Cl P) /\ [#]D as non empty Subset of D by A15,A16,A19,XBOOLE_0:def 4; not p in P by A1,A10,A11,CONNSP_1:35,A4,A9,XBOOLE_0:3; then p in P` by SUBSET_1:29; then reconsider F3 = P` /\ [#]D as non empty Subset of D by A18,XBOOLE_0:def 4; set T1 = D|F1; set T3 = D|F3; A20: the carrier of T1 = F1 by PRE_TOPC:8; A21: the carrier of T3 = F3 by PRE_TOPC:8; A22: the carrier of T2|B1 = B1 by PRE_TOPC:8; A23: A c= B proof let a be object; assume a in A; then A24: a in C by A2; then a in Ball(p,r) by A3; hence thesis by A12,A16,A17,A24,ZFMISC_1:56; end; A25: F1 c= B proof let a be object; assume A26: a in F1; then A27: a in Cl P by XBOOLE_0:def 4; not p in Cl P by A4,XBOOLE_0:3,A1,A9,A10,A11,Th68; hence thesis by A12,A15,A26,A27,ZFMISC_1:56; end; then reconsider f1 = id F1 as Function of T1,T2B1 by A20,A22,FUNCT_2:7; f|F3 is Function of F3,A by A14; then reconsider g1 = f|F3 as Function of T3,T2B1 by A21,A22,A23,FUNCT_2:7; A28: F1 = [#]T1 by PRE_TOPC:8; A29: F3 = [#]T3 by PRE_TOPC:8; A30: [#]T1 \/ [#]T3 = [#]D proof thus [#]T1 \/ [#]T3 c= [#]D by A28,A29,XBOOLE_1:8; let p be object; assume A31: p in [#]D; per cases; suppose p in P; then p in F1 by A19,A31,XBOOLE_0:def 4; hence thesis by A28,XBOOLE_0:def 3; end; suppose not p in P; then p in P` by A15,A31,SUBSET_1:29; then p in F3 by A31,XBOOLE_0:def 4; hence thesis by A29,XBOOLE_0:def 3; end; end; reconsider DT = [#]D as closed Subset of T2 by BORSUK_1:def 11,TSEP_1:1; DT /\ Cl P is closed; then A32: F1 is closed by TSEP_1:8; P is_a_component_of C` by A9,A10; then P is open by SPRECT_3:8; then DT /\ P` is closed; then A33: F3 is closed by TSEP_1:8; A34: id T1 = id F1 by PRE_TOPC:8; T1 is SubSpace of T2 by TSEP_1:7; then T1 is SubSpace of T2B1 by A20,A22,A25,TSEP_1:4; then A35: f1 is continuous by A34,PRE_TOPC:26; A36: T2|A is SubSpace of T2B1 by A14,A22,A23,TSEP_1:4; reconsider g2 = g1 as Function of T3,T2|A by A21; g2 is continuous by A7,TOPMETR:7; then A37: g1 is continuous by A36,PRE_TOPC:26; A38: for x being set st x in Cl P & x in P` holds f.x = x proof let x be set; assume that A39: x in Cl P and A40: x in P`; A41: x in Cl P /\ P` by A39,A40,XBOOLE_0:def 4; then (id A).x = x by A5,FUNCT_1:18; hence thesis by A5,A8,A41,FUNCT_1:49; end; for x being object st x in [#]T1 /\ [#]T3 holds f1.x = g1.x proof let x be object; assume A42: x in [#]T1 /\ [#]T3; then A43: x in [#]T1 by XBOOLE_0:def 4; then A44: x in Cl P by A28,XBOOLE_0:def 4; x in P` by A29,A42,XBOOLE_0:def 4; then A45: f.x = x by A38,A44; thus f1.x = x by A28,A43,FUNCT_1:18 .= g1.x by A29,A42,A45,FUNCT_1:49; end; then consider g being Function of D,T2|B such that A46: g = f1+*g1 and A47: g is continuous by A28,A29,A30,A32,A33,A35,A37,JGRAPH_2:1; take g; thus g is continuous by A47; let x be Point of D; A48: dom g1 = the carrier of T3 by FUNCT_2:def 1; hereby assume A49: x in Cl P; then A50: x in F1 by XBOOLE_0:def 4; per cases; suppose not x in dom g1; hence g.x = f1.x by A46,FUNCT_4:11 .= x by A50,FUNCT_1:18; end; suppose A51: x in dom g1; then A52: x in P` by A21,XBOOLE_0:def 4; thus g.x = g1.x by A46,A51,FUNCT_4:13 .= f.x by A21,A51,FUNCT_1:49 .= x by A38,A49,A52; end; end; assume x in P`; then A53: x in F3 by XBOOLE_0:def 4; hence g.x = g1.x by A21,A46,A48,FUNCT_4:13 .= f.x by A53,FUNCT_1:49; end; Lm15: BDD C is non empty & U = P & U is a_component implies C = Fr P proof assume that A1: BDD C is non empty and A2: U = P and A3: U is a_component and A4: C <> Fr P; A5: the carrier of T2|C` = C` by PRE_TOPC:8; reconsider T2C = T2|C` as non empty SubSpace of T2; A6: T2C is locally_connected by JORDAN2C:81; then U is open by A3,CONNSP_2:15; then reconsider P as open Subset of T2 by A2,TSEP_1:17; A7: Fr P = Cl P /\ P` by PRE_TOPC:22; set Z = {X where X is Subset of T2|C`: X is a_component & X <> U}; set V = union Z; A8: V \/ U \/ C = the carrier of T2 proof A9: V c= the carrier of T2 proof let a be object; assume a in V; then consider A being set such that A10: a in A and A11: A in Z by TARSKI:def 4; ex X being Subset of T2|C` st X = A & X is a_component & X <> U by A11; hence thesis by A5,A10,TARSKI:def 3; end; U c= the carrier of T2 by A5,XBOOLE_1:1; then V \/ U c= the carrier of T2 by A9,XBOOLE_1:8; hence V \/ U \/ C c= the carrier of T2 by XBOOLE_1:8; let a be object; assume A12: a in the carrier of T2; per cases; suppose a in C; hence thesis by XBOOLE_0:def 3; end; suppose not a in C; then reconsider a as Point of T2|C` by A5,A12,SUBSET_1:29; A13: a in Component_of a by CONNSP_1:38; per cases; suppose Component_of a = U; then a in V \/ U by A13,XBOOLE_0:def 3; hence thesis by XBOOLE_0:def 3; end; suppose A14: Component_of a <> U; Component_of a is a_component by CONNSP_1:40; then Component_of a in Z by A14; then a in V by A13,TARSKI:def 4; then a in V \/ U by XBOOLE_0:def 3; hence thesis by XBOOLE_0:def 3; end; end; end; A15: P misses P` by XBOOLE_1:79; Fr P c= C proof let a be object; assume A16: a in Fr P; then A17: a in Cl P by XBOOLE_0:def 4; A18: a in P` by A7,A16,XBOOLE_0:def 4; assume not a in C; then a in V \/ U by A8,A16,XBOOLE_0:def 3; then a in V or a in U by XBOOLE_0:def 3; then consider O being set such that A19: a in O and A20: O in Z by A2,A15,A18,TARSKI:def 4,XBOOLE_0:3; consider X being Subset of T2|C` such that A21: X = O and A22: X is a_component and A23: X <> U by A20; Cl P misses X by A2,A3,A22,A23,Th68; hence thesis by A17,A19,A21,XBOOLE_0:3; end; then Fr P c< C by A4; then consider p1, p2, A such that A24: A is_an_arc_of p1,p2 and A25: Fr P c= A and A26: A c= C by BORSUK_4:59; A27: U <> {}(T2|C`) by A3,CONNSP_1:32; per cases; suppose P is bounded; then reconsider P as bounded Subset of T2; consider p being object such that A28: p in U by A27,XBOOLE_0:def 1; reconsider p as Point of T2 by A2,A28; A29: P \/ C is bounded by TOPREAL6:67; then reconsider PC = P \/ C as bounded Subset of Euclid 2 by JORDAN2C:11; consider r being positive Real such that A30: PC c= Ball(p,r) by A29,Th26; C c= PC by XBOOLE_1:7; then A31: C c= Ball(p,r) by A30; set D = Tdisk(p,r); set S = Tcircle(p,r); set B = cl_Ball(p,r) \ {p}; A32: the carrier of S = Sphere(p,r) by TOPREALB:9; A33: the carrier of D = cl_Ball(p,r) by BROUWER:3; A34: Sphere(p,r) c= cl_Ball(p,r) by TOPREAL9:17; A35: Ball(p,r) misses Sphere(p,r) by TOPREAL9:19; A36: Ball(p,r) c= cl_Ball(p,r) by TOPREAL9:16; A c= Ball(p,r) by A26,A31; then A is Subset of D by A33,A36,XBOOLE_1:1; then consider R being Function of D, T2|A such that A37: R is continuous and A38: R|A = id A by A24,Lm12; P c= PC by XBOOLE_1:7; then A39: P c= Ball(p,r) by A30; then consider f being Function of D, T2|B such that A40: f is continuous and A41: for x being Point of D holds (x in Cl P implies f.x = R.x) & (x in P` implies f.x = x) by A2,A3,A7,A24,A25,A26,A28,A31,A37,A38,Lm13; set g = DiskProj(p,r,p); set h = RotateCircle(p,r,p); A42: S is SubSpace of D by A32,A33,A34,TSEP_1:4; reconsider F = h*(g*f) as Function of D,D by A32,A33,A34,FUNCT_2:7; p is Point of D by Th17; then A43: g is continuous by Th64; |. p-p .| = 0 by TOPRNS_1:28; then A44: p in Ball(p,r) by TOPREAL9:7; then h is continuous by Th66; then A45: F is continuous by A40,A42,A43,PRE_TOPC:26; now let x be object; per cases; suppose A46: x in dom F; A47: Ball(p,r) \/ Sphere(p,r) = cl_Ball(p,r) by TOPREAL9:18; now per cases by A33,A46,A47,XBOOLE_0:def 3; suppose A48: x in Ball(p,r); F.x in the carrier of S by A46,FUNCT_2:5; hence F.x <> x by A32,A35,A48,XBOOLE_0:3; end; suppose A49: x in Sphere(p,r); A50: dom f = the carrier of D by FUNCT_2:def 1; not x in P by A35,A39,A49,XBOOLE_0:3; then A51: x in P` by A49,SUBSET_1:29; A52: g|Sphere(p,r) = id Sphere(p,r) by A44,Th65; h is without_fixpoints by A44,Th67; then A53: not x is_a_fixpoint_of h; A54: dom h = the carrier of S by FUNCT_2:def 1; F.x = h.((g*f).x) by A46,FUNCT_1:12 .= h.(g.(f.x)) by A33,A34,A49,A50,FUNCT_1:13 .= h.(g.x) by A33,A34,A41,A49,A51 .= h.((id Sphere(p,r)).x) by A49,A52,FUNCT_1:49 .= h.x by A49,FUNCT_1:18; hence F.x <> x by A32,A49,A53,A54; end; end; hence not x is_a_fixpoint_of F; end; suppose not x in dom F; hence not x is_a_fixpoint_of F; end; end; then not F is with_fixpoint; hence thesis by A45,BROUWER:14; end; suppose A55: not P is bounded; consider p being object such that A56: p in BDD C by A1; consider Z being set such that A57: p in Z and A58: Z in {B where B is Subset of T2: B is_inside_component_of C} by A56,TARSKI:def 4; consider P1 being Subset of T2 such that A59: Z = P1 and A60: P1 is_inside_component_of C by A58; consider U1 being Subset of T2|C` such that A61: U1 = P1 and A62: U1 is a_component and U1 is bounded Subset of Euclid 2 by A60,JORDAN2C:13; U1 is open by A6,A62,CONNSP_2:15; then reconsider P1 as non empty open bounded Subset of T2 by A57,A59,A60,A61,TSEP_1:17; reconsider p as Point of T2 by A57,A59; A63: p in P1 by A57,A59; A64: P1 \/ C is bounded by TOPREAL6:67; then reconsider PC = P1 \/ C as bounded Subset of Euclid 2 by JORDAN2C:11; consider rv being positive Real such that A65: PC c= Ball(p,rv) by A64,Th26; not P c= Ball(p,rv) by A55,RLTOPSP1:42; then consider u being object such that A66: u in P and A67: not u in Ball(p,rv); reconsider u as Point of T2 by A66; set r = |.u-p.|; P misses P1 by A2,A3,A55,A61,A62,CONNSP_1:35; then p <> u by A57,A59,A66,XBOOLE_0:3; then reconsider r as non zero non negative Real by TOPRNS_1:28; A68: r >= rv by A67,TOPREAL9:7; then Ball(p,rv) c= Ball(p,r) by Th18; then A69: PC c= Ball(p,r) by A65; A70: Fr Ball(p,r) = Sphere(p,r) by Th24; u in Sphere(p,r) by TOPREAL9:9; then A71: P meets Ball(p,r) by A66,A70,TOPS_1:28; A72: C c= PC by XBOOLE_1:7; then A73: C c= Ball(p,r) by A69; set D = Tdisk(p,r); set S = Tcircle(p,r); set B = cl_Ball(p,r) \ {p}; A74: the carrier of S = Sphere(p,r) by TOPREALB:9; A75: the carrier of D = cl_Ball(p,r) by BROUWER:3; A76: Sphere(p,r) c= cl_Ball(p,r) by TOPREAL9:17; A77: Ball(p,r) misses Sphere(p,r) by TOPREAL9:19; A78: Ball(p,r) c= cl_Ball(p,r) by TOPREAL9:16; A c= Ball(p,r) by A26,A73; then A is Subset of D by A75,A78,XBOOLE_1:1; then consider R being Function of D, T2|A such that A79: R is continuous and A80: R|A = id A by A24,Lm12; p1 in A by A24,TOPREAL1:1; then consider f being Function of D, T2|B such that A81: f is continuous and A82: for x being Point of D holds (x in Cl P implies f.x = x) & (x in P` implies f.x = R.x) by A2,A3,A7,A25,A26,A55,A61,A62,A63,A71,A73,A79,A80,Lm14; set g = DiskProj(p,r,p); set h = RotateCircle(p,r,p); A83: S is SubSpace of D by A74,A75,A76,TSEP_1:4; reconsider F = h*(g*f) as Function of D,D by A74,A75,A76,FUNCT_2:7; p is Point of D by Th17; then A84: g is continuous by Th64; |. p-p .| = 0 by TOPRNS_1:28; then A85: p in Ball(p,r) by TOPREAL9:7; then h is continuous by Th66; then A86: F is continuous by A81,A83,A84,PRE_TOPC:26; now let x be object; per cases; suppose A87: x in dom F; A88: Ball(p,r) \/ Sphere(p,r) = cl_Ball(p,r) by TOPREAL9:18; now per cases by A75,A87,A88,XBOOLE_0:def 3; suppose A89: x in Ball(p,r); F.x in the carrier of S by A87,FUNCT_2:5; hence F.x <> x by A74,A77,A89,XBOOLE_0:3; end; suppose A90: x in Sphere(p,r); A91: dom f = the carrier of D by FUNCT_2:def 1; A92: P c= Cl P by PRE_TOPC:18; set SS = Sphere(p,r); SS c= C` proof let a be object; assume A93: a in SS; assume not a in C`; then A94: a in C by A93,SUBSET_1:29; reconsider a as Point of T2 by A93; a in PC by A72,A94; then |.a-p.| < rv by A65,TOPREAL9:7; hence contradiction by A68,A93,TOPREAL9:9; end; then reconsider SS as Subset of T2|C` by PRE_TOPC:8; A95: u in SS by TOPREAL9:9; SS is connected by CONNSP_1:23; then SS misses U or SS c= U by A3,CONNSP_1:36; then A96: x in P by A2,A66,A90,A95,XBOOLE_0:3; A97: g|Sphere(p,r) = id Sphere(p,r) by A85,Th65; h is without_fixpoints by A85,Th67; then A98: not x is_a_fixpoint_of h; A99: dom h = the carrier of S by FUNCT_2:def 1; F.x = h.((g*f).x) by A87,FUNCT_1:12 .= h.(g.(f.x)) by A75,A76,A90,A91,FUNCT_1:13 .= h.(g.x) by A75,A76,A82,A90,A92,A96 .= h.((id Sphere(p,r)).x) by A90,A97,FUNCT_1:49 .= h.x by A90,FUNCT_1:18; hence F.x <> x by A74,A90,A98,A99; end; end; hence not x is_a_fixpoint_of F; end; suppose not x in dom F; hence not x is_a_fixpoint_of F; end; end; then F is without_fixpoints; hence thesis by A86,BROUWER:14; end; end; set rp = 1; set rl = -rp; set rg = 3; set rd = -rg; set a = |[rl,0]|; set b = |[rp,0]|; set c = |[0,rg]|; set d = |[0,rd]|; set lg = |[rl,rg]|; set pg = |[rp,rg]|; set ld = |[rl,rd]|; set pd = |[rp,rd]|; set R = closed_inside_of_rectangle(rl,rp,rd,rg); set dR = rectangle(rl,rp,rd,rg); set TR = Trectangle(rl,rp,rd,rg); Lm16: a`1 = rl by EUCLID:52; Lm17: b`1 = rp by EUCLID:52; Lm18: a`2 = 0 by EUCLID:52; Lm19: b`2 = 0 by EUCLID:52; Lm20: c`1 = 0 by EUCLID:52; Lm21: c`2 = rg by EUCLID:52; Lm22: d`1 = 0 by EUCLID:52; Lm23: d`2 = rd by EUCLID:52; Lm24: lg`1 = rl by EUCLID:52; Lm25: lg`2 = rg by EUCLID:52; Lm26: ld`1 = rl by EUCLID:52; Lm27: ld`2 = rd by EUCLID:52; Lm28: pg`1 = rp by EUCLID:52; Lm29: pg`2 = rg by EUCLID:52; Lm30: pd`1 = rp by EUCLID:52; Lm31: pd`2 = rd by EUCLID:52; Lm32: ld = |[ld`1,ld`2]| by EUCLID:53; Lm33: lg = |[lg`1,lg`2]| by EUCLID:53; Lm34: pd = |[pd`1,pd`2]| by EUCLID:53; Lm35: pg = |[pg`1,pg`2]| by EUCLID:53; Lm36: dR = (LSeg(ld,lg) \/ LSeg(lg,pg)) \/ (LSeg(pg,pd) \/ LSeg(pd,ld)) by SPPOL_2:def 3; Lm37: LSeg(ld,lg) c= LSeg(ld,lg) \/ LSeg(lg,pg) by XBOOLE_1:7; LSeg(ld,lg) \/ LSeg(lg,pg) c= dR by Lm36,XBOOLE_1:7; then Lm38: LSeg(ld,lg) c= dR by Lm37; Lm39: LSeg(lg,pg) c= LSeg(ld,lg) \/ LSeg(lg,pg) by XBOOLE_1:7; LSeg(ld,lg) \/ LSeg(lg,pg) c= dR by Lm36,XBOOLE_1:7; then Lm40: LSeg(lg,pg) c= dR by Lm39; Lm41: LSeg(pg,pd) c= LSeg(pg,pd) \/ LSeg(pd,ld) by XBOOLE_1:7; LSeg(pg,pd) \/ LSeg(pd,ld) c= dR by Lm36,XBOOLE_1:7; then Lm42: LSeg(pg,pd) c= dR by Lm41; Lm43: LSeg(pd,ld) c= LSeg(pg,pd) \/ LSeg(pd,ld) by XBOOLE_1:7; LSeg(pg,pd) \/ LSeg(pd,ld) c= dR by Lm36,XBOOLE_1:7; then Lm44: LSeg(pd,ld) c= dR by Lm43; Lm45: LSeg(ld,lg) is vertical by Lm24,Lm26,SPPOL_1:16; Lm46: LSeg(pd,pg) is vertical by Lm28,Lm30,SPPOL_1:16; Lm47: LSeg(a,lg) is vertical by Lm16,Lm24,SPPOL_1:16; Lm48: LSeg(a,ld) is vertical by Lm16,Lm26,SPPOL_1:16; Lm49: LSeg(b,pg) is vertical by Lm17,Lm28,SPPOL_1:16; Lm50: LSeg(b,pd) is vertical by Lm17,Lm30,SPPOL_1:16; Lm51: LSeg(ld,d) is horizontal by Lm23,Lm27,SPPOL_1:15; Lm52: LSeg(pd,d) is horizontal by Lm23,Lm31,SPPOL_1:15; Lm53: LSeg(lg,c) is horizontal by Lm21,Lm25,SPPOL_1:15; Lm54: LSeg(pg,c) is horizontal by Lm21,Lm29,SPPOL_1:15; Lm55: LSeg(lg,pg) is horizontal by Lm25,Lm29,SPPOL_1:15; Lm56: LSeg(ld,pd) is horizontal by Lm27,Lm31,SPPOL_1:15; Lm57: LSeg(a,lg) c= LSeg(ld,lg) by Lm16,Lm18,Lm25,Lm26,Lm27,Lm45,Lm47,GOBOARD7:63; Lm58: LSeg(a,ld) c= LSeg(ld,lg) by Lm18,Lm25,Lm26,Lm27,Lm45,Lm48,GOBOARD7:63; Lm59: LSeg(b,pg) c= LSeg(pd,pg) by Lm17,Lm19,Lm29,Lm30,Lm31,Lm46,Lm49,GOBOARD7:63; Lm60: LSeg(b,pd) c= LSeg(pd,pg) by Lm19,Lm29,Lm30,Lm31,Lm46,Lm50,GOBOARD7:63; Lm61: dR = {p where p is Point of T2: p`1 = rl & p`2 <= rg & p`2 >= rd or p`1 <= rp & p`1 >= rl & p`2 = rg or p`1 <= rp & p`1 >= rl & p`2 = rd or p`1 = rp & p`2 <= rg & p`2 >= rd} by SPPOL_2:54; then Lm62: c in dR by Lm20,Lm21; Lm63: d in dR by Lm22,Lm23,Lm61; Lm64: (2+1)^2 = 4 + 4 + 1; then Lm65: sqrt(9) = 3 by SQUARE_1:def 2; Lm66: dist(a,b) = sqrt ((a`1-b`1)^2 + (a`2-b`2)^2) by TOPREAL6:92 .= --2 by Lm16,Lm17,Lm18,Lm19,SQUARE_1:23; theorem Th70: for h being Homeomorphism of TOP-REAL 2 holds h.:C is being_simple_closed_curve proof let h be Homeomorphism of T2; consider f being Function of T2|R^2-unit_square, T2|C such that A1: f is being_homeomorphism by TOPREAL2:def 1; reconsider g = h|C as Function of T2|C,T2|(h.:C) by JORDAN24:12; take g*f; g is being_homeomorphism by JORDAN24:14; hence thesis by A1,TOPS_2:57; end; theorem Th71: |[-1,0]|,|[1,0]| realize-max-dist-in P implies P c= closed_inside_of_rectangle(-1,1,-3,3) proof assume that A1: a in P and A2: b in P and A3: for x, y being Point of TOP-REAL 2 st x in P & y in P holds dist(a,b) >= dist(x,y); let p be object; assume A4: p in P; then reconsider p as Point of TOP-REAL 2; A5: dist(a,p) = sqrt((rl-p`1)^2 + (0-p`2)^2) by Lm16,Lm18,TOPREAL6:92 .= sqrt((rl-p`1)^2 + p`2^2); A6: now assume 9 < p`2^2; then 0+9 < (rl-p`1)^2+p`2^2 by XREAL_1:8; then 3 < sqrt((rl-p`1)^2+p`2^2) by Lm65,SQUARE_1:27; then 2 < sqrt((rl-p`1)^2+p`2^2) by XXREAL_0:2; hence contradiction by A1,A3,A4,A5,Lm66; end; A7: now assume A8: rl > p`1; then LSeg(p,b) meets Vertical_Line(rl) by Lm17,Th8; then consider x being object such that A9: x in LSeg(p,b) and A10: x in Vertical_Line(rl) by XBOOLE_0:3; reconsider x as Point of T2 by A9; A11: x`1 = rl by A10,JORDAN6:31; A12: dist(p,b) = dist(p,x)+dist(x,b) by A9,JORDAN1K:29; A13: dist(x,b) = sqrt((x`1-b`1)^2 + (x`2-b`2)^2) by TOPREAL6:92 .= sqrt((-2)^2 + (x`2-0)^2) by A11,Lm17,EUCLID:52 .= sqrt(4 + x`2^2); now assume dist(x,b) < dist(a,b); then 4 + x`2^2 < 4 + 0 by A13,Lm66,SQUARE_1:20,26; hence contradiction by XREAL_1:6; end; then dist(p,b) + 0 > dist(a,b) + 0 by A8,A11,A12,JORDAN1K:22,XREAL_1:8; hence contradiction by A2,A3,A4; end; A14: now assume A15: p`1 > rp; then LSeg(p,a) meets Vertical_Line(rp) by Lm16,Th8; then consider x being object such that A16: x in LSeg(p,a) and A17: x in Vertical_Line(rp) by XBOOLE_0:3; reconsider x as Point of T2 by A16; A18: x`1 = rp by A17,JORDAN6:31; A19: dist(p,a) = dist(p,x)+dist(x,a) by A16,JORDAN1K:29; A20: dist(x,a) = sqrt((x`1-a`1)^2 + (x`2-a`2)^2) by TOPREAL6:92 .= sqrt(4 + x`2^2) by A18,Lm16,Lm18; now assume dist(x,a) < dist(a,b); then 4 + x`2^2 < 4 + 0 by A20,Lm66,SQUARE_1:20,26; hence contradiction by XREAL_1:6; end; then dist(p,a) + 0 > dist(a,b) + 0 by A15,A18,A19,JORDAN1K:22,XREAL_1:8; hence contradiction by A1,A3,A4; end; A21: now assume rd > p`2; then p`2^2 > rd^2 by SQUARE_1:44; hence contradiction by A6; end; rg >= p`2 by A6,Lm64,SQUARE_1:16; hence thesis by A7,A14,A21; end; Lm67: dR c= R by Th45; Lm68: lg`2 = lg`2; Lm69: lg`1 <= c`1 by Lm24,EUCLID:52; c`1 <= pg`1 by Lm28,EUCLID:52; then LSeg(lg,c) c= LSeg(lg,pg) by Lm53,Lm55,Lm68,Lm69,GOBOARD7:64; then Lm70: LSeg(lg,c) c= dR by Lm40; LSeg(pg,c) c= LSeg(lg,pg) by Lm20,Lm21,Lm24,Lm25,Lm28,Lm54,Lm55,GOBOARD7:64; then Lm71: LSeg(pg,c) c= dR by Lm40; Lm72: ld`2 = ld`2; Lm73: ld`1 <= d`1 by Lm26,EUCLID:52; d`1 <= pd`1 by Lm30,EUCLID:52; then LSeg(ld,d) c= LSeg(ld,pd) by Lm51,Lm56,Lm72,Lm73,GOBOARD7:64; then Lm74: LSeg(ld,d) c= dR by Lm44; LSeg(pd,d) c= LSeg(ld,pd) by Lm22,Lm23,Lm26,Lm27,Lm30,Lm52,Lm56,GOBOARD7:64; then Lm75: LSeg(pd,d) c= dR by Lm44; Lm76: 0 <= p`2 & p in dR implies p in LSeg(a,lg) or p in LSeg(lg,c) or p in LSeg(c,pg) or p in LSeg(pg,b) proof assume A1: 0 <= p`2; assume p in dR; then consider p1 such that A2: p1 = p and A3: p1`1 = rl & p1`2 <= rg & p1`2 >= rd or p1`1 <= rp & p1`1 >= rl & p1`2 = rg or p1`1 <= rp & p1`1 >= rl & p1`2 = rd or p1`1 = rp & p1`2 <= rg & p1`2 >= rd by Lm61; per cases by A3; suppose p1`1 = rl & p1`2 <= rg & p1`2 >= rd; hence thesis by A1,A2,Lm16,Lm18,Lm24,Lm25,GOBOARD7:7; end; suppose A4: p1`1 <= rp & p1`1 >= rl & p1`2 = rg; per cases; suppose p1`1 <= c`1; hence thesis by A2,A4,Lm21,Lm24,Lm25,GOBOARD7:8; end; suppose c`1 <= p1`1; hence thesis by A2,A4,Lm21,Lm28,Lm29,GOBOARD7:8; end; end; suppose p1`1 <= rp & p1`1 >= rl & p1`2 = rd; hence thesis by A1,A2; end; suppose p1`1 = rp & p1`2 <= rg & p1`2 >= rd; hence thesis by A1,A2,Lm17,Lm19,Lm28,Lm29,GOBOARD7:7; end; end; Lm77: p`2 <= 0 & p in dR implies p in LSeg(a,ld) or p in LSeg(ld,d) or p in LSeg(d,pd) or p in LSeg(pd,b) proof assume A1: p`2 <= 0; assume p in dR; then consider p1 such that A2: p1 = p and A3: p1`1 = rl & p1`2 <= rg & p1`2 >= rd or p1`1 <= rp & p1`1 >= rl & p1`2 = rg or p1`1 <= rp & p1`1 >= rl & p1`2 = rd or p1`1 = rp & p1`2 <= rg & p1`2 >= rd by Lm61; per cases by A3; suppose p1`1 = rl & p1`2 <= rg & p1`2 >= rd; hence thesis by A1,A2,Lm16,Lm18,Lm26,Lm27,GOBOARD7:7; end; suppose p1`1 <= rp & p1`1 >= rl & p1`2 = rg; hence thesis by A1,A2; end; suppose A4: p1`1 <= rp & p1`1 >= rl & p1`2 = rd; per cases; suppose p1`1 <= d`1; hence thesis by A2,A4,Lm23,Lm26,Lm27,GOBOARD7:8; end; suppose d`1 <= p1`1; hence thesis by A2,A4,Lm23,Lm30,Lm31,GOBOARD7:8; end; end; suppose p1`1 = rp & p1`2 <= rg & p1`2 >= rd; hence thesis by A1,A2,Lm17,Lm19,Lm30,Lm31,GOBOARD7:7; end; end; theorem Th72: |[-1,0]|,|[1,0]| realize-max-dist-in P implies P misses LSeg(|[-1,3]|,|[1,3]|) proof assume A1: a,b realize-max-dist-in P; assume P meets LSeg(lg,pg); then consider x being object such that A2: x in P and A3: x in LSeg(lg,pg) by XBOOLE_0:3; reconsider x as Point of T2 by A2; lg in LSeg(lg,pg) by RLTOPSP1:68; then A4: x`2 = rg by A3,Lm25,Lm55; A5: dist(a,x) = sqrt ((a`1-x`1)^2 + (a`2-x`2)^2) by TOPREAL6:92 .= sqrt ((rl-x`1)^2 + rg^2) by A4,Lm18,EUCLID:52; 0+4 < (rl-x`1)^2+9 by XREAL_1:8; then 2 < dist(a,x) by A5,SQUARE_1:20,27; hence thesis by A1,A2,Lm66; end; theorem Th73: |[-1,0]|,|[1,0]| realize-max-dist-in P implies P misses LSeg(|[-1,-3]|,|[1,-3]|) proof assume A1: a,b realize-max-dist-in P; assume P meets LSeg(ld,pd); then consider x being object such that A2: x in P and A3: x in LSeg(ld,pd) by XBOOLE_0:3; reconsider x as Point of T2 by A2; ld in LSeg(ld,pd) by RLTOPSP1:68; then A4: x`2 = rd by A3,Lm27,Lm56; A5: dist(a,x) = sqrt ((a`1-x`1)^2 + (a`2-x`2)^2) by TOPREAL6:92 .= sqrt ((rl-x`1)^2 + (-rd)^2) by A4,Lm18,EUCLID:52; 0+4 < (rl-x`1)^2+9 by XREAL_1:8; then 2 < dist(a,x) by A5,SQUARE_1:20,27; hence thesis by A1,A2,Lm66; end; theorem Th74: |[-1,0]|,|[1,0]| realize-max-dist-in P implies P /\ rectangle(-1,1,-3,3) = {|[-1,0]|,|[1,0]|} proof assume A1: a,b realize-max-dist-in P; then A2: a in P; A3: b in P by A1; thus P /\ dR c= {a,b} proof let x be object; assume A4: x in P /\ dR; then A5: x in P by XBOOLE_0:def 4; x in dR by A4,XBOOLE_0:def 4; then A6: x in LSeg(ld,lg) \/ LSeg(lg,pg) or x in LSeg(pg,pd) \/ LSeg(pd,ld) by Lm36,XBOOLE_0:def 3; reconsider x as Point of T2 by A4; per cases by A6,XBOOLE_0:def 3; suppose A7: x in LSeg(ld,lg); ld in LSeg(ld,lg) by RLTOPSP1:68; then A8: x`1 = rl by A7,Lm26,Lm45; per cases; suppose x`2 = 0; then x = a by A8,Lm16,Lm18,TOPREAL3:6; hence thesis by TARSKI:def 2; end; suppose x`2 <> 0; then A9: x`2^2 > 0 by SQUARE_1:12; A10: dist(b,x) = sqrt ((rp-rl)^2 + (0-x`2)^2) by A8,Lm17,Lm19,TOPREAL6:92 .= sqrt (4 + x`2^2); 0+4 < x`2^2+4 by A9,XREAL_1:6; then 2 < sqrt(x`2^2+4) by SQUARE_1:20,27; hence thesis by A1,A5,A10,Lm66; end; end; suppose x in LSeg(lg,pg); then LSeg(lg,pg) meets P by A5,XBOOLE_0:3; hence thesis by A1,Th72; end; suppose A11: x in LSeg(pg,pd); pd in LSeg(pd,pg) by RLTOPSP1:68; then A12: x`1 = rp by A11,Lm30,Lm46; per cases; suppose x`2 = 0; then x = b by A12,Lm17,Lm19,TOPREAL3:6; hence thesis by TARSKI:def 2; end; suppose x`2 <> 0; then A13: x`2^2 > 0 by SQUARE_1:12; A14: dist(x,a) = sqrt ((x`1-a`1)^2 + (x`2-a`2)^2) by TOPREAL6:92 .= sqrt (4 + x`2^2) by A12,Lm16,Lm18; 0+4 < x`2^2+4 by A13,XREAL_1:6; then 2 < sqrt(x`2^2+4) by SQUARE_1:20,27; hence thesis by A1,A5,A14,Lm66; end; end; suppose x in LSeg(pd,ld); then LSeg(pd,ld) meets P by A5,XBOOLE_0:3; hence thesis by A1,Th73; end; end; let x be object; assume x in {a,b}; then A15: x = a or x = b by TARSKI:def 2; A16: a in dR by Lm16,Lm18,Lm61; b in dR by Lm17,Lm19,Lm61; hence thesis by A2,A3,A15,A16,XBOOLE_0:def 4; end; Lm78: |[-1,0]|,|[1,0]| realize-max-dist-in C implies LSeg(lg,c) misses C proof assume a,b realize-max-dist-in C; then A1: C /\ dR = {a,b} by Th74; assume LSeg(lg,c) meets C; then consider q being object such that A2: q in LSeg(lg,c) and A3: q in C by XBOOLE_0:3; reconsider q as Point of T2 by A3; q in dR /\ C by A2,A3,Lm70,XBOOLE_0:def 4; then q = a or q = b by A1,TARSKI:def 2; hence contradiction by A2,Lm18,Lm19,TOPREAL3:12; end; Lm79: |[-1,0]|,|[1,0]| realize-max-dist-in C implies LSeg(pg,c) misses C proof assume a,b realize-max-dist-in C; then A1: C /\ dR = {a,b} by Th74; assume LSeg(pg,c) meets C; then consider q being object such that A2: q in LSeg(pg,c) and A3: q in C by XBOOLE_0:3; reconsider q as Point of T2 by A3; q in dR /\ C by A2,A3,Lm71,XBOOLE_0:def 4; then q = a or q = b by A1,TARSKI:def 2; hence contradiction by A2,Lm18,Lm19,TOPREAL3:12; end; Lm80: |[-1,0]|,|[1,0]| realize-max-dist-in C implies LSeg(ld,d) misses C proof assume a,b realize-max-dist-in C; then A1: C /\ dR = {a,b} by Th74; assume LSeg(ld,d) meets C; then consider q being object such that A2: q in LSeg(ld,d) and A3: q in C by XBOOLE_0:3; reconsider q as Point of T2 by A3; q in dR /\ C by A2,A3,Lm74,XBOOLE_0:def 4; then q = a or q = b by A1,TARSKI:def 2; hence contradiction by A2,Lm18,Lm19,TOPREAL3:12; end; Lm81: |[-1,0]|,|[1,0]| realize-max-dist-in C implies LSeg(pd,d) misses C proof assume a,b realize-max-dist-in C; then A1: C /\ dR = {a,b} by Th74; assume LSeg(pd,d) meets C; then consider q being object such that A2: q in LSeg(pd,d) and A3: q in C by XBOOLE_0:3; reconsider q as Point of T2 by A3; q in dR /\ C by A2,A3,Lm75,XBOOLE_0:def 4; then q = a or q = b by A1,TARSKI:def 2; hence contradiction by A2,Lm18,Lm19,TOPREAL3:12; end; Lm82: |[ -1,0]|,|[1,0]| realize-max-dist-in C & p in C` & p in LSeg(a,lg) implies LSeg(p,lg) misses C proof assume that A1: a,b realize-max-dist-in C and A2: p in C` and A3: p in LSeg(a,lg); A4: C /\ dR = {a,b} by A1,Th74; assume LSeg(p,lg) meets C; then consider q being object such that A5: q in LSeg(p,lg) and A6: q in C by XBOOLE_0:3; reconsider q as Point of T2 by A6; lg in LSeg(a,lg) by RLTOPSP1:68; then A7: p`1 = lg`1 by A3,Lm47; A8: p`2 <= lg`2 by A3,Lm25,JGRAPH_6:1; A9: LSeg(p,lg) is vertical by A7,SPPOL_1:16; a`2 <= p`2 by A3,Lm18,JGRAPH_6:1; then LSeg(p,lg) c= LSeg(ld,lg) by A7,A8,A9,Lm18,Lm24,Lm26,Lm27,Lm45,GOBOARD7:63; then LSeg(p,lg) c= dR by Lm38; then q in dR /\ C by A5,A6,XBOOLE_0:def 4; then A10: q = a or q = b by A4,TARSKI:def 2; a in LSeg(a,lg) by RLTOPSP1:68; then A11: a`1 = p`1 by A3,Lm47; A12: a in C by A1; not p in C by A2,XBOOLE_0:def 5; then a`2 <> p`2 by A11,A12,TOPREAL3:6; then A13: a`2 < p`2 by A3,Lm18,JGRAPH_6:1; p = |[p`1,p`2]| by EUCLID:53; hence contradiction by A5,A7,A8,A10,A13,Lm17,Lm24,Lm33,JGRAPH_6:1; end; Lm83: |[ -1,0]|,|[1,0]| realize-max-dist-in C & p in C` & p in LSeg(b,pg) implies LSeg(p,pg) misses C proof assume that A1: a,b realize-max-dist-in C and A2: p in C` and A3: p in LSeg(b,pg); A4: C /\ dR = {a,b} by A1,Th74; assume LSeg(p,pg) meets C; then consider q being object such that A5: q in LSeg(p,pg) and A6: q in C by XBOOLE_0:3; reconsider q as Point of T2 by A6; pg in LSeg(b,pg) by RLTOPSP1:68; then A7: p`1 = pg`1 by A3,Lm49; A8: p`2 <= pg`2 by A3,Lm29,JGRAPH_6:1; A9: LSeg(p,pg) is vertical by A7,SPPOL_1:16; b`2 <= p`2 by A3,Lm19,JGRAPH_6:1; then LSeg(p,pg) c= LSeg(pd,pg) by A7,A8,A9,Lm19,Lm28,Lm30,Lm31,Lm46,GOBOARD7:63; then LSeg(p,pg) c= dR by Lm42; then q in dR /\ C by A5,A6,XBOOLE_0:def 4; then A10: q = a or q = b by A4,TARSKI:def 2; b in LSeg(b,pg) by RLTOPSP1:68; then A11: b`1 = p`1 by A3,Lm49; A12: b in C by A1; not p in C by A2,XBOOLE_0:def 5; then b`2 <> p`2 by A11,A12,TOPREAL3:6; then A13: b`2 < p`2 by A3,Lm19,JGRAPH_6:1; p = |[p`1,p`2]| by EUCLID:53; hence contradiction by A5,A7,A8,A10,A13,Lm16,Lm28,Lm35,JGRAPH_6:1; end; Lm84: |[ -1,0]|,|[1,0]| realize-max-dist-in C & p in C` & p in LSeg(a,ld) implies LSeg(p,ld) misses C proof assume that A1: a,b realize-max-dist-in C and A2: p in C` and A3: p in LSeg(a,ld); A4: C /\ dR = {a,b} by A1,Th74; assume LSeg(p,ld) meets C; then consider q being object such that A5: q in LSeg(p,ld) and A6: q in C by XBOOLE_0:3; reconsider q as Point of T2 by A6; ld in LSeg(a,ld) by RLTOPSP1:68; then A7: p`1 = ld`1 by A3,Lm48; A8: ld`2 <= p`2 by A3,Lm27,JGRAPH_6:1; A9: LSeg(p,ld) is vertical by A7,SPPOL_1:16; p`2 <= a`2 by A3,Lm18,JGRAPH_6:1; then LSeg(p,ld) c= LSeg(ld,lg) by A7,A8,A9,Lm18,Lm25,Lm45,GOBOARD7:63; then LSeg(p,ld) c= dR by Lm38; then q in dR /\ C by A5,A6,XBOOLE_0:def 4; then A10: q = a or q = b by A4,TARSKI:def 2; a in LSeg(a,ld) by RLTOPSP1:68; then A11: a`1 = p`1 by A3,Lm48; A12: a in C by A1; not p in C by A2,XBOOLE_0:def 5; then a`2 <> p`2 by A11,A12,TOPREAL3:6; then A13: p`2 < a`2 by A3,Lm18,JGRAPH_6:1; p = |[p`1,p`2]| by EUCLID:53; hence contradiction by A5,A7,A8,A10,A13,Lm17,Lm26,Lm32,JGRAPH_6:1; end; Lm85: |[ -1,0]|,|[1,0]| realize-max-dist-in C & p in C` & p in LSeg(b,pd) implies LSeg(p,pd) misses C proof assume that A1: a,b realize-max-dist-in C and A2: p in C` and A3: p in LSeg(b,pd); A4: C /\ dR = {a,b} by A1,Th74; assume LSeg(p,pd) meets C; then consider q being object such that A5: q in LSeg(p,pd) and A6: q in C by XBOOLE_0:3; reconsider q as Point of T2 by A6; pd in LSeg(b,pd) by RLTOPSP1:68; then A7: p`1 = pd`1 by A3,Lm50; A8: pd`2 <= p`2 by A3,Lm31,JGRAPH_6:1; A9: LSeg(p,pd) is vertical by A7,SPPOL_1:16; p`2 <= b`2 by A3,Lm19,JGRAPH_6:1; then LSeg(p,pd) c= LSeg(pd,pg) by A7,A8,A9,Lm19,Lm29,Lm46,GOBOARD7:63; then LSeg(p,pd) c= dR by Lm42; then q in dR /\ C by A5,A6,XBOOLE_0:def 4; then A10: q = a or q = b by A4,TARSKI:def 2; b in LSeg(b,pd) by RLTOPSP1:68; then A11: b`1 = p`1 by A3,Lm50; A12: b in C by A1; not p in C by A2,XBOOLE_0:def 5; then b`2 <> p`2 by A11,A12,TOPREAL3:6; then A13: p`2 < b`2 by A3,Lm19,JGRAPH_6:1; p = |[p`1,p`2]| by EUCLID:53; hence contradiction by A5,A7,A8,A10,A13,Lm16,Lm30,Lm34,JGRAPH_6:1; end; Lm86: |[0,r]| in rectangle(rl,rp,rd,rg) implies r = rd or r = rg proof assume |[0,r]| in dR; then ex p st p = |[0,r]| & (p`1 = rl & p`2 <= rg & p`2 >= rd or p`1 <= rp & p`1 >= rl & p`2 = rg or p`1 <= rp & p`1 >= rl & p`2 = rd or p`1 = rp & p`2 <= rg & p`2 >= rd) by Lm61; hence thesis by EUCLID:52; end; theorem Th75: |[-1,0]|,|[1,0]| realize-max-dist-in P implies W-bound P = -1 proof assume A1: a,b realize-max-dist-in P; then A2: P c= R by Th71; A3: P = the carrier of (T2|P) by PRE_TOPC:8; A4: a in P by A1; reconsider P as non empty Subset of T2 by A1; reconsider Z = (proj1|P).:the carrier of (T2|P) as Subset of REAL; A5: for p be Real st p in Z holds p >= rl proof let p be Real; assume p in Z; then consider p0 being object such that A6: p0 in the carrier of T2|P and p0 in the carrier of T2|P and A7: p = (proj1|P).p0 by FUNCT_2:64; p0 in R by A2,A3,A6; then ex p1 st p0 = p1 & rl <= p1`1 & p1`1 <= rp & rd <= p1`2 & p1`2 <= rg; hence thesis by A3,A6,A7,PSCOMP_1:22; end; for q being Real st for p being Real st p in Z holds p >= q holds rl >= q proof let q be Real such that A8: for p being Real st p in Z holds p >= q; (proj1|P).a = a`1 by A4,PSCOMP_1:22; hence thesis by A3,A4,A8,Lm16,FUNCT_2:35; end; hence thesis by A5,SEQ_4:44; end; theorem Th76: |[-1,0]|,|[1,0]| realize-max-dist-in P implies E-bound P = 1 proof assume A1: a,b realize-max-dist-in P; then A2: P c= R by Th71; A3: b in P by A1; reconsider P as non empty Subset of T2 by A1; reconsider Z = (proj1|P).:the carrier of (T2|P) as Subset of REAL; A4: P = the carrier of (T2|P) by PRE_TOPC:8; A5: for p be Real st p in Z holds p <= rp proof let p be Real; assume p in Z; then consider p0 being object such that A6: p0 in the carrier of T2|P and p0 in the carrier of T2|P and A7: p = (proj1|P).p0 by FUNCT_2:64; p0 in R by A2,A4,A6; then ex p1 st p0 = p1 & rl <= p1`1 & p1`1 <= rp & rd <= p1`2 & p1`2 <= rg; hence thesis by A4,A6,A7,PSCOMP_1:22; end; for q being Real st for p being Real st p in Z holds p <= q holds rp <= q proof let q be Real such that A8: for p being Real st p in Z holds p <= q; (proj1|P).b = b`1 by A3,PSCOMP_1:22; hence thesis by A3,A4,A8,Lm17,FUNCT_2:35; end; hence thesis by A5,SEQ_4:46; end; theorem Th77: for P being compact Subset of TOP-REAL 2 holds |[-1,0]|,|[1,0]| realize-max-dist-in P implies W-most P = {|[-1,0]|} proof let P be compact Subset of T2; assume A1: a,b realize-max-dist-in P; then A2: P c= R by Th71; set L = LSeg(SW-corner P, NW-corner P); A3: a in P by A1; A4: (SW-corner P)`1 = |[rl,S-bound P]|`1 by A1,Th75 .= rl by EUCLID:52; A5: (NW-corner P)`1 = |[rl,N-bound P]|`1 by A1,Th75 .= rl by EUCLID:52; thus W-most P c= {a} proof let x be object; assume A6: x in W-most P; then A7: x in P by XBOOLE_0:def 4; reconsider x as Point of T2 by A6; A8: x in L by A6,XBOOLE_0:def 4; SW-corner P in L by RLTOPSP1:68; then A9: x`1 = rl by A4,A8,SPPOL_1:def 3; x in R by A2,A7; then ex p st x = p & rl <= p`1 & p`1 <= rp & rd <= p`2 & p`2 <= rg; then x in dR by A9,Lm61; then x in P /\ dR by A7,XBOOLE_0:def 4; then x in {a,b} by A1,Th74; then x = a or x = b by TARSKI:def 2; hence thesis by A9,EUCLID:52,TARSKI:def 1; end; let x be object; assume x in {a}; then A10: x = a by TARSKI:def 1; A11: (SW-corner P)`2 = S-bound P by EUCLID:52; A12: (NW-corner P)`2 = N-bound P by EUCLID:52; A13: (SW-corner P)`2 <= a`2 by A3,A11,PSCOMP_1:24; a`2 <= (NW-corner P)`2 by A3,A12,PSCOMP_1:24; then a in L by A4,A5,A13,Lm16,GOBOARD7:7; hence thesis by A3,A10,XBOOLE_0:def 4; end; theorem Th78: for P being compact Subset of TOP-REAL 2 holds |[-1,0]|,|[1,0]| realize-max-dist-in P implies E-most P = {|[1,0]|} proof let P be compact Subset of T2; assume A1: a,b realize-max-dist-in P; then A2: P c= R by Th71; set L = LSeg(SE-corner P, NE-corner P); A3: b in P by A1; A4: (SE-corner P)`1 = |[rp,S-bound P]|`1 by A1,Th76 .= rp by EUCLID:52; A5: (NE-corner P)`1 = |[rp,N-bound P]|`1 by A1,Th76 .= rp by EUCLID:52; thus E-most P c= {b} proof let x be object; assume A6: x in E-most P; then A7: x in P by XBOOLE_0:def 4; reconsider x as Point of T2 by A6; A8: x in L by A6,XBOOLE_0:def 4; SE-corner P in L by RLTOPSP1:68; then A9: x`1 = rp by A4,A8,SPPOL_1:def 3; x in R by A2,A7; then ex p st x = p & rl <= p`1 & p`1 <= rp & rd <= p`2 & p`2 <= rg; then x in dR by A9,Lm61; then x in P /\ dR by A7,XBOOLE_0:def 4; then x in {a,b} by A1,Th74; then x = a or x = b by TARSKI:def 2; hence thesis by A9,EUCLID:52,TARSKI:def 1; end; let x be object; assume x in {b}; then A10: x = b by TARSKI:def 1; A11: (SE-corner P)`2 = S-bound P by EUCLID:52; A12: (NE-corner P)`2 = N-bound P by EUCLID:52; A13: (SE-corner P)`2 <= b`2 by A3,A11,PSCOMP_1:24; b`2 <= (NE-corner P)`2 by A3,A12,PSCOMP_1:24; then b in L by A4,A5,A13,Lm17,GOBOARD7:7; hence thesis by A3,A10,XBOOLE_0:def 4; end; theorem Th79: for P being compact Subset of TOP-REAL 2 holds |[-1,0]|,|[1,0]| realize-max-dist-in P implies W-min P = |[-1,0]| & W-max P = |[-1,0]| proof let P be compact Subset of T2; set M = W-most P; assume A1: a,b realize-max-dist-in P; then A2: M = {a} by Th77; set f = proj2|M; A3: dom f = the carrier of (T2|M) by FUNCT_2:def 1; A4: the carrier of (T2|M) = M by PRE_TOPC:8; A5: a in {a} by TARSKI:def 1; A6: f.:the carrier of (T2|M) = Im(f,a) by A1,A4,Th77 .= {f.a} by A2,A3,A4,A5,FUNCT_1:59 .= {proj2.a} by A2,A5,FUNCT_1:49 .= {a`2} by PSCOMP_1:def 6; then A7: lower_bound (proj2|M) = a`2 by SEQ_4:9; A8: upper_bound (proj2|M) = a`2 by A6,SEQ_4:9; a = |[a`1,a`2]| by EUCLID:53; hence thesis by A1,A7,A8,Lm16,Th75; end; theorem Th80: for P being compact Subset of TOP-REAL 2 holds |[-1,0]|,|[1,0]| realize-max-dist-in P implies E-min P = |[1,0]| & E-max P = |[1,0]| proof let P be compact Subset of T2; set M = E-most P; assume A1: a,b realize-max-dist-in P; then A2: M = {b} by Th78; set f = proj2|M; A3: dom f = the carrier of (T2|M) by FUNCT_2:def 1; A4: the carrier of (T2|M) = M by PRE_TOPC:8; A5: b in {b} by TARSKI:def 1; A6: f.:the carrier of (T2|M) = Im(f,b) by A1,A4,Th78 .= {f.b} by A2,A3,A4,A5,FUNCT_1:59 .= {proj2.b} by A2,A5,FUNCT_1:49 .= {b`2} by PSCOMP_1:def 6; then A7: lower_bound (proj2|M) = b`2 by SEQ_4:9; A8: upper_bound (proj2|M) = b`2 by A6,SEQ_4:9; b = |[b`1,b`2]| by EUCLID:53; hence thesis by A1,A7,A8,Lm17,Th76; end; Lm87: |[-1,0]|,|[1,0]| realize-max-dist-in P implies c`1 = (W-bound P + E-bound P) / 2 proof assume A1: a,b realize-max-dist-in P; then A2: W-bound P = rl by Th75; E-bound P = rp by A1,Th76; hence thesis by A2,EUCLID:52; end; Lm88: |[-1,0]|,|[1,0]| realize-max-dist-in P implies d`1 = (W-bound P + E-bound P) / 2 proof assume A1: a,b realize-max-dist-in P; then A2: W-bound P = rl by Th75; E-bound P = rp by A1,Th76; hence thesis by A2,EUCLID:52; end; theorem Th81: |[-1,0]|,|[1,0]| realize-max-dist-in P implies LSeg(|[0,3]|,UMP P) is vertical proof assume a,b realize-max-dist-in P; then c`1 = (W-bound P + E-bound P) / 2 by Lm87 .= (UMP P)`1 by EUCLID:52; hence thesis by SPPOL_1:16; end; theorem Th82: |[-1,0]|,|[1,0]| realize-max-dist-in P implies LSeg(LMP P,|[0,-3]|) is vertical proof assume a,b realize-max-dist-in P; then d`1 = (W-bound P + E-bound P) / 2 by Lm88 .= (LMP P)`1 by EUCLID:52; hence thesis by SPPOL_1:16; end; theorem Th83: |[-1,0]|,|[1,0]| realize-max-dist-in P & p in P implies p`2 < 3 proof assume that A1: a,b realize-max-dist-in P and A2: p in P; A3: P /\ dR = {a,b} by A1,Th74; P c= R by A1,Th71; then p in R by A2; then A4: ex p1 st p1 = p & rl <= p1`1 & p1`1 <= rp & rd <= p1`2 & p1`2 <= rg; now assume A5: p`2 = c`2; then p in LSeg(lg,pg) by A4,Lm21,Lm24,Lm25,Lm28,Lm29,GOBOARD7:8; then p in P /\ dR by A2,Lm40,XBOOLE_0:def 4; hence contradiction by A3,A5,Lm18,Lm19,Lm21,TARSKI:def 2; end; hence thesis by A4,Lm21,XXREAL_0:1; end; theorem Th84: |[-1,0]|,|[1,0]| realize-max-dist-in P & p in P implies -3 < p`2 proof assume that A1: a,b realize-max-dist-in P and A2: p in P; A3: P /\ dR = {a,b} by A1,Th74; P c= R by A1,Th71; then p in R by A2; then A4: ex p1 st p1 = p & rl <= p1`1 & p1`1 <= rp & rd <= p1`2 & p1`2 <= rg; now assume A5: p`2 = d`2; then p in LSeg(ld,pd) by A4,Lm23,Lm26,Lm27,Lm30,Lm31,GOBOARD7:8; then p in P /\ dR by A2,Lm44,XBOOLE_0:def 4; then p = a or p = b by A3,TARSKI:def 2; hence contradiction by A5,Lm23,EUCLID:52; end; hence thesis by A4,Lm23,XXREAL_0:1; end; theorem Th85: |[-1,0]|,|[1,0]| realize-max-dist-in D & p in LSeg(|[0,3]|,UMP D) implies (UMP D)`2 <= p`2 proof set x = UMP D; assume that A1: a,b realize-max-dist-in D and A2: p in LSeg(c,x); A3: x in LSeg(c,x) by RLTOPSP1:68; A4: LSeg(c,x) is vertical by A1,Th81; A5: c = |[c`1,c`2]| by EUCLID:53; A6: x = |[x`1,x`2]| by EUCLID:53; c in LSeg(c,x) by RLTOPSP1:68; then A7: c`1 = x`1 by A3,A4; x`2 <= c`2 by A1,Lm21,Th83,JORDAN21:30; hence thesis by A2,A5,A6,A7,JGRAPH_6:1; end; theorem Th86: |[-1,0]|,|[1,0]| realize-max-dist-in D & p in LSeg(LMP D,|[0,-3]|) implies p`2 <= (LMP D)`2 proof set x = LMP D; assume that A1: a,b realize-max-dist-in D and A2: p in LSeg(x,d); A3: x in LSeg(x,d) by RLTOPSP1:68; A4: LSeg(x,d) is vertical by A1,Th82; A5: d = |[d`1,d`2]| by EUCLID:53; A6: x = |[x`1,x`2]| by EUCLID:53; d in LSeg(x,d) by RLTOPSP1:68; then A7: d`1 = x`1 by A3,A4; d`2 <= x`2 by A1,Lm23,Th84,JORDAN21:31; hence thesis by A2,A5,A6,A7,JGRAPH_6:1; end; theorem Th87: |[-1,0]|,|[1,0]| realize-max-dist-in D implies LSeg(|[0,3]|,UMP D) c= north_halfline UMP D proof set p = UMP D; assume A1: a,b realize-max-dist-in D; let x be object; assume A2: x in LSeg(c,p); then reconsider x as Point of T2; A3: p in LSeg(c,p) by RLTOPSP1:68; LSeg(c,p) is vertical by A1,Th81; then A4: x`1 = p`1 by A2,A3; p`2 <= x`2 by A1,A2,Th85; hence thesis by A4,TOPREAL1:def 10; end; theorem Th88: |[-1,0]|,|[1,0]| realize-max-dist-in D implies LSeg(LMP D,|[0,-3]|) c= south_halfline LMP D proof set p = LMP D; assume A1: a,b realize-max-dist-in D; let x be object; assume A2: x in LSeg(p,d); then reconsider x as Point of T2; A3: p in LSeg(p,d) by RLTOPSP1:68; A4: LSeg(p,d) is vertical by A1,Th82; then A5: x`1 = p`1 by A2,A3; A6: d = |[d`1,d`2]| by EUCLID:53; A7: p = |[p`1,p`2]| by EUCLID:53; d in LSeg(p,d) by RLTOPSP1:68; then A8: d`1 = p`1 by A3,A4; d`2 <= p`2 by A1,Lm23,Th84,JORDAN21:31; then x`2 <= p`2 by A2,A6,A7,A8,JGRAPH_6:1; hence thesis by A5,TOPREAL1:def 12; end; theorem Th89: |[-1,0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C implies LSeg(|[0,3]|,UMP C) misses P proof set m = UMP C; set L = LSeg(c,m); assume that A1: a,b realize-max-dist-in C and A2: P is_inside_component_of C; A3: ex VP being Subset of T2|C` st ( VP = P)&( VP is a_component)&( VP is bounded Subset of Euclid 2) by A2,JORDAN2C:13; m in L by RLTOPSP1:68; then {m} c= L by ZFMISC_1:31; then A4: L = L \ {m} \/ {m} by XBOOLE_1:45; A5: L \ {m} c= north_halfline m \ {m} by A1,Th87,XBOOLE_1:33; north_halfline m \ {m} c= UBD C by Th12; then L \ {m} c= UBD C by A5; then A6: L \ {m} misses P by A2,Th14,XBOOLE_1:63; {m} misses P by A3,Lm4,JORDAN21:30; hence thesis by A4,A6,XBOOLE_1:70; end; theorem Th90: |[-1,0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C implies LSeg(LMP C,|[0,-3]|) misses P proof set m = LMP C; set L = LSeg(m,d); assume that A1: a,b realize-max-dist-in C and A2: P is_inside_component_of C; A3: ex VP being Subset of T2|C` st ( VP = P)&( VP is a_component)&( VP is bounded Subset of Euclid 2) by A2,JORDAN2C:13; m in L by RLTOPSP1:68; then {m} c= L by ZFMISC_1:31; then A4: L = L \ {m} \/ {m} by XBOOLE_1:45; A5: L \ {m} c= south_halfline m \ {m} by A1,Th88,XBOOLE_1:33; south_halfline m \ {m} c= UBD C by Th13; then L \ {m} c= UBD C by A5; then A6: L \ {m} misses P by A2,Th14,XBOOLE_1:63; {m} misses P by A3,Lm4,JORDAN21:31; hence thesis by A4,A6,XBOOLE_1:70; end; theorem Th91: |[-1,0]|,|[1,0]| realize-max-dist-in D implies LSeg(|[0,3]|,UMP D) /\ D = {UMP D} proof assume A1: a,b realize-max-dist-in D; set m = UMP D; set w = (W-bound D + E-bound D) / 2; A2: c`1 = w by A1,Lm87; A3: m`1 = w by EUCLID:52; A4: m in LSeg(c,m) by RLTOPSP1:68; A5: m in D by JORDAN21:30; thus LSeg(c,m) /\ D c= {m} proof let x be object; assume A6: x in LSeg(c,m) /\ D; then A7: x in LSeg(c,m) by XBOOLE_0:def 4; A8: x in D by A6,XBOOLE_0:def 4; reconsider x as Point of T2 by A6; LSeg(c,m) is vertical by A2,A3,SPPOL_1:16; then A9: x`1 = m`1 by A4,A7; then x in Vertical_Line w by A3,JORDAN6:31; then x in D /\ Vertical_Line w by A8,XBOOLE_0:def 4; then A10: x`2 <= m`2 by JORDAN21:28; m`2 <= x`2 by A1,A7,Th85; then x`2 = m`2 by A10,XXREAL_0:1; then x = m by A9,TOPREAL3:6; hence thesis by TARSKI:def 1; end; let x be object; assume x in {m}; then x = m by TARSKI:def 1; hence thesis by A4,A5,XBOOLE_0:def 4; end; theorem |[-1,0]|,|[1,0]| realize-max-dist-in D implies LSeg(|[0,-3]|,LMP D) /\ D = {LMP D} proof assume A1: a,b realize-max-dist-in D; set m = LMP D; set w = (W-bound D + E-bound D) / 2; A2: d`1 = w by A1,Lm88; A3: m`1 = w by EUCLID:52; A4: m in LSeg(d,m) by RLTOPSP1:68; A5: m in D by JORDAN21:31; thus LSeg(d,m) /\ D c= {m} proof let x be object; assume A6: x in LSeg(d,m) /\ D; then A7: x in LSeg(d,m) by XBOOLE_0:def 4; A8: x in D by A6,XBOOLE_0:def 4; reconsider x as Point of T2 by A6; LSeg(d,m) is vertical by A2,A3,SPPOL_1:16; then A9: x`1 = m`1 by A4,A7; then x in Vertical_Line w by A3,JORDAN6:31; then x in D /\ Vertical_Line w by A8,XBOOLE_0:def 4; then A10: m`2 <= x`2 by JORDAN21:29; x`2 <= m`2 by A1,A7,Th86; then x`2 = m`2 by A10,XXREAL_0:1; then x = m by A9,TOPREAL3:6; hence thesis by TARSKI:def 1; end; let x be object; assume x in {m}; then x = m by TARSKI:def 1; hence thesis by A4,A5,XBOOLE_0:def 4; end; theorem Th93: P is compact & |[-1,0]|,|[1,0]| realize-max-dist-in P & A is_inside_component_of P implies A c= closed_inside_of_rectangle(-1,1,-3,3) proof assume that A1: P is compact and A2: |[-1,0]|,|[1,0]| realize-max-dist-in P and A3: A is_inside_component_of P; let x be object; assume that A4: x in A and A5: not x in R; P c= R by A2,Th71; then A6: R` c= P` by SUBSET_1:12; reconsider x as Point of T2 by A4; A7: not (rl <= x`1 & x`1 <= rp & rd <= x`2 & x`2 <= rg) by A5; per cases; suppose A8: 0 <= x`1; set E = east_halfline(x); E c= R` proof let e be object; assume A9: e in E; then reconsider e as Point of T2; A10: e`1 >= x`1 by A9,TOPREAL1:def 11; now assume e in R; then ex p st e = p & rl <= p`1 & p`1 <= rp & rd <= p`2 & p`2 <= rg; hence contradiction by A7,A8,A9,A10,TOPREAL1:def 11,XXREAL_0:2; end; hence thesis by SUBSET_1:29; end; then E c= P` by A6; then E misses P by SUBSET_1:23; then A11: E c= UBD P by A1,JORDAN2C:127; x in E by TOPREAL1:38; then A meets UBD P by A4,A11,XBOOLE_0:3; hence thesis by A3,Th14; end; suppose A12: x`1 < 0; set E = west_halfline(x); E c= R` proof let e be object; assume A13: e in E; then reconsider e as Point of T2; A14: e`1 <= x`1 by A13,TOPREAL1:def 13; now assume e in R; then ex p st e = p & rl <= p`1 & p`1 <= rp & rd <= p`2 & p`2 <= rg; hence contradiction by A7,A12,A13,A14,TOPREAL1:def 13,XXREAL_0:2; end; hence thesis by SUBSET_1:29; end; then E c= P` by A6; then E misses P by SUBSET_1:23; then A15: E c= UBD P by A1,JORDAN2C:126; x in E by TOPREAL1:38; then A meets UBD P by A4,A15,XBOOLE_0:3; hence thesis by A3,Th14; end; end; Lm89: p in R implies R c= Ball(p,10) proof assume p in R; then consider p1 such that A1: p1 = p and A2: rl <= p1`1 and A3: p1`1 <= rp and A4: rd <= p1`2 and A5: p1`2 <= rg; let x be object; assume A6: x in R; then reconsider x as Point of T2; consider p2 such that A7: p2 = x and A8: rl <= p2`1 and A9: p2`1 <= rp and A10: rd <= p2`2 and A11: p2`2 <= rg by A6; A12: ex s, t being Point of Euclid 2 st s = p1 & t = p2 & dist(p1,p2) = dist(s,t) by TOPREAL6:def 1; dist(p1,p2) <= (rp-rl) + (rg-rd) by A2,A3,A4,A5,A8,A9,A10,A11,TOPREAL6:95; then dist(p1,p2) < 10 by XXREAL_0:2; then |.x-p.| < 10 by A1,A7,A12,SPPOL_1:39; hence thesis by TOPREAL9:7; end; theorem |[-1,0]|,|[1,0]| realize-max-dist-in C implies LSeg(|[0,3]|,|[0,-3]|) meets C proof assume A1: a,b realize-max-dist-in C; set Jc = Upper_Arc C; consider Pf being Path of c,d, f being Function of I[01], T2|LSeg(c,d) such that A2: rng f = LSeg(c,d) and A3: Pf = f by Th43; A4: a = W-min C by A1,Th79; b = E-max C by A1,Th80; then Jc is_an_arc_of a,b by A4,JORDAN6:def 8; then consider Pg being Path of a,b, g being Function of I[01], T2|Jc such that A5: rng g = Jc and A6: Pg = g by Th42; A7: Jc c= C by JORDAN6:61; A8: C c= R by A1,Th71; A9: a in C by A1; A10: b in C by A1; A11: the carrier of TR = R by PRE_TOPC:8; reconsider AR = a, BR = b, CR = c, DR = d as Point of TR by A8,A9,A10,Lm62,Lm63,Lm67,PRE_TOPC:8; rng Pg c= the carrier of TR by A5,A6,A7,A8,A11; then reconsider h = Pg as Path of AR,BR by Th30; LSeg(c,d) c= R by Lm62,Lm63,Lm67,JORDAN1:def 1; then reconsider v = Pf as Path of CR,DR by A2,A3,A11,Th30; consider s, t being Point of I[01] such that A12: h.s = v.t by Lm16,Lm17,Lm21,Lm23,JGRAPH_8:6; A13: dom h = the carrier of I[01] by FUNCT_2:def 1; dom v = the carrier of I[01] by FUNCT_2:def 1; then A14: v.t in rng Pf by FUNCT_1:def 3; h.s in rng Pg by A13,FUNCT_1:def 3; hence thesis by A2,A3,A5,A6,A7,A12,A14,XBOOLE_0:3; end; Lm90: |[-1,0]|,|[1,0]| realize-max-dist-in C implies ex Jc, Jd being compact with_the_max_arc Subset of T2 st Jc is_an_arc_of |[-1,0]|,|[1,0]| & Jd is_an_arc_of |[-1,0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[-1,0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc proof assume A1: a,b realize-max-dist-in C; set U = Upper_Arc C; set L = Lower_Arc C; A2: U \/ L = C by JORDAN6:def 9; A3: UMP C in C by JORDAN21:30; LMP C in C by JORDAN21:31; then A4: LMP C in U or LMP C in L by A2,XBOOLE_0:def 3; A5: W-min C = a by A1,Th79; A6: E-max C = b by A1,Th80; per cases by A2,A3,XBOOLE_0:def 3; suppose A7: UMP C in U; take U, L; thus thesis by A4,A5,A6,A7,JORDAN21:17,18,50,JORDAN6:50; end; suppose A8: UMP C in L; take L, U; thus thesis by A4,A5,A6,A8,JORDAN21:19,20,49,JORDAN6:50; end; end; theorem Th95: |[-1,0]|,|[1,0]| realize-max-dist-in C implies for Jc, Jd being compact with_the_max_arc Subset of TOP-REAL 2 st Jc is_an_arc_of |[-1,0]|,|[1,0]| & Jd is_an_arc_of |[-1,0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[-1,0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc for Ux being Subset of TOP-REAL 2 st Ux = Component_of Down ((1/2) * ((UMP (LSeg(LMP Jc,|[0,-3]|) /\ Jd)) + LMP Jc), C`) holds Ux is_inside_component_of C & for V being Subset of TOP-REAL 2 st V is_inside_component_of C holds V = Ux proof set m = UMP C; set j = LMP C; assume A1: a,b realize-max-dist-in C; let Jc, Jd being compact with_the_max_arc Subset of T2 such that A2: Jc is_an_arc_of a,b and A3: Jd is_an_arc_of a,b and A4: C = Jc \/ Jd and A5: Jc /\ Jd = {a,b} and A6: UMP C in Jc and A7: LMP C in Jd and A8: W-bound C = W-bound Jc and A9: E-bound C = E-bound Jc; set l = LMP Jc; set LJ = LSeg(l,d) /\ Jd; set k = UMP LJ; set x = (1/2)*(k+l); set w = (W-bound C + E-bound C) / 2; let Ux be Subset of TOP-REAL 2 such that A10: Ux = Component_of Down (x,C`); A11: C c= R by A1,Th71; A12: W-bound C = rl by A1,Th75; A13: E-bound C = rp by A1,Th76; A14: a in C by A1; A15: b in C by A1; A16: m in C by JORDAN21:30; A17: l in Jc by JORDAN21:31; A18: Jd c= C by A4,XBOOLE_1:7; A19: Jc c= C by A4,XBOOLE_1:7; then A20: l in C by A17; A21: m`2 < c`2 by A1,Lm21,Th83,JORDAN21:30; A22: l`1 = 0 by A8,A9,A12,A13,EUCLID:52; A23: c`1 = w by A1,Lm87; A24: m`1 = w by EUCLID:52; A25: m <> a by A12,A13,Lm16,EUCLID:52; A26: m <> b by A12,A13,Lm17,EUCLID:52; A27: l <> a by A8,A9,A12,A13,Lm16,EUCLID:52; A28: l <> b by A8,A9,A12,A13,Lm17,EUCLID:52; then consider Pml being Path of m,l such that A29: rng Pml c= Jc and A30: rng Pml misses {a,b} by A2,A6,A17,A25,A26,A27,Th44; set ml = rng Pml; A31: ml c= C by A19,A29; A32: j in C by A7,A18; A33: LSeg(l,d) is vertical by A22,Lm22,SPPOL_1:16; A34: d`2 <= j`2 by A1,A7,A18,Lm23,Th84; A35: j`1 = 0 by A12,A13,EUCLID:52; l in Vertical_Line w by A12,A13,A22,JORDAN6:31; then A36: l in C /\ Vertical_Line w by A17,A19,XBOOLE_0:def 4; then j`2 <= l`2 by JORDAN21:29; then j in LSeg(l,d) by A22,A34,A35,Lm22,GOBOARD7:7; then A37: LJ is non empty by A7,XBOOLE_0:def 4; A38: LJ is vertical by A33,Th4; then A39: k in LJ by A37,JORDAN21:30; then A40: k in LSeg(l,d) by XBOOLE_0:def 4; A41: k in Jd by A39,XBOOLE_0:def 4; then A42: k in C by A18; A43: d in LSeg(l,d) by RLTOPSP1:68; then A44: k`1 = 0 by A33,A40,Lm22; then A45: k <> a by EUCLID:52; A46: k <> b by A44,EUCLID:52; A47: j <> a by A35,EUCLID:52; j <> b by A35,EUCLID:52; then consider Pkj being Path of k,j such that A48: rng Pkj c= Jd and A49: rng Pkj misses {a,b} by A3,A7,A41,A45,A46,A47,Th44; set kj = rng Pkj; A50: kj c= C by A18,A48; A51: x in LSeg(k,l) by RLTOPSP1:69; A52: Component_of Down(x,C`) is a_component by CONNSP_1:40; A53: the carrier of T2|C` = C` by PRE_TOPC:8; A54: LSeg(l,k) is vertical by A22,A44,SPPOL_1:16; A55: k in LSeg(l,k) by RLTOPSP1:68; A56: l = |[l`1,l`2]| by EUCLID:53; A57: k = |[k`1,k`2]| by EUCLID:53; A58: d = |[d`1,d`2]| by EUCLID:53; d`2 <= l`2 by A1,A17,A19,Lm23,Th84; then A59: k`2 <= l`2 by A22,A40,A56,A58,Lm22,JGRAPH_6:1; A60: a <> k by A44,EUCLID:52; b <> k by A44,EUCLID:52; then not k in {a,b} by A60,TARSKI:def 2; then A61: k <> l by A5,A17,A41,XBOOLE_0:def 4; then k`2 <> l`2 by A22,A44,TOPREAL3:6; then A62: k`2 < l`2 by A59,XXREAL_0:1; k in Vertical_Line w by A12,A13,A44,JORDAN6:31; then k in C /\ Vertical_Line w by A18,A41,XBOOLE_0:def 4; then j`2 <= k`2 by JORDAN21:29; then d`2 <= k`2 by A1,A7,A18,Lm23,Th84,XXREAL_0:2; then A63: LSeg(l,k) c= LSeg(l,d) by A33,A44,A54,A59,Lm22,GOBOARD7:63; A64: LSeg(l,k) \ {l,k} c= C` proof let q be object; assume that A65: q in LSeg(l,k) \ {l,k} and A66: not q in C`; A67: q in LSeg(l,k) by A65,XBOOLE_0:def 5; reconsider q as Point of T2 by A65; A68: q in C by A66,SUBSET_1:29; A69: q`1 = w by A12,A13,A44,A54,A55,A67; then A70: q in Vertical_Line w by JORDAN6:31; per cases by A4,A68,XBOOLE_0:def 3; suppose q in Jc; then q in Jc /\ Vertical_Line w by A70,XBOOLE_0:def 4; then A71: l`2 <= q`2 by A8,A9,JORDAN21:29; q`2 <= l`2 by A22,A44,A56,A57,A59,A67,JGRAPH_6:1; then l`2 = q`2 by A71,XXREAL_0:1; then l = q by A12,A13,A22,A69,TOPREAL3:6; then q in {l,k} by TARSKI:def 2; hence contradiction by A65,XBOOLE_0:def 5; end; suppose q in Jd; then A72: q in LJ by A63,A67,XBOOLE_0:def 4; A73: q`1 = d`1 by A33,A43,A63,A67; A74: W-bound LSeg(l,d) <= W-bound LJ by A72,PSCOMP_1:69,XBOOLE_1:17; A75: E-bound LJ <= E-bound LSeg(l,d) by A72,PSCOMP_1:67,XBOOLE_1:17; A76: W-bound LJ = E-bound LJ by A37,A38,SPRECT_1:15; A77: W-bound LSeg(l,d) = d`1 by A22,Lm22,SPRECT_1:54; then W-bound LSeg(l,d) = W-bound LJ by A22,A74,A75,A76,Lm22,SPRECT_1:57; then q in Vertical_Line ((W-bound LJ + E-bound LJ) / 2) by A73,A76,A77,JORDAN6:31; then q in LJ /\ Vertical_Line ((W-bound LJ + E-bound LJ) / 2) by A72,XBOOLE_0:def 4; then A78: q`2 <= k`2 by JORDAN21:28; k`2 <= q`2 by A22,A44,A56,A57,A59,A67,JGRAPH_6:1; then k`2 = q`2 by A78,XXREAL_0:1; then k = q by A12,A13,A44,A69,TOPREAL3:6; then q in {l,k} by TARSKI:def 2; hence contradiction by A65,XBOOLE_0:def 5; end; end; then reconsider X = LSeg(l,k) \ {l,k} as Subset of T2|C` by PRE_TOPC:8; now assume x in {l,k}; then x = l or x = k by TARSKI:def 2; hence contradiction by A61,Th1; end; then A79: x in LSeg(l,k) \ {l,k} by A51,XBOOLE_0:def 5; then Component_of(x,C`) = Component_of Down(x,C`) by A64,CONNSP_3:27; then A80: x in Component_of Down(x,C`) by A64,A79,CONNSP_3:26; then A81: X meets Ux by A10,A79,XBOOLE_0:3; LSeg(l,k) \ {l,k} is convex by JORDAN1:46; then X is connected by CONNSP_1:23; then A82: X c= Component_of Down(x,C`) by A10,A52,A81,CONNSP_1:36; A83: LSeg(l,k) c= R by A11,A20,A42,JORDAN1:def 1; A84: the carrier of TR = R by PRE_TOPC:8; reconsider AR = a, BR = b, CR = c, DR = d as Point of TR by A11,A14,A15,Lm62,Lm63,Lm67,PRE_TOPC:8; consider Pcm being Path of c,m, fcm being Function of I[01], T2|LSeg(c,m) such that A85: rng fcm = LSeg(c,m) and A86: Pcm = fcm by Th43; A87: LSeg(c,m) c= R by A11,A16,Lm62,Lm67,JORDAN1:def 1; A88: ml c= R by A11,A31; thus Ux is_inside_component_of C proof thus A89: Ux is_a_component_of C` by A10,A52; assume not Ux is bounded; then not Ux c= Ball(x,10) by RLTOPSP1:42; then consider u being object such that A90: u in Ux and A91: not u in Ball(x,10); A92: R c= Ball(x,10) by A51,A83,Lm89; reconsider u as Point of T2 by A90; A93: Ux is open by A89,SPRECT_3:8; Component_of Down(x,C`) is connected by A52; then A94: Ux is connected by A10,CONNSP_1:23; x in Ball(x,10) by Th16; then consider P1 being Subset of T2 such that A95: P1 is_S-P_arc_joining x,u and A96: P1 c= Ux by A10,A80,A90,A91,A93,A94,TOPREAL4:29; A97: P1 is_an_arc_of x,u by A95,TOPREAL4:2; reconsider P2 = P1 as Subset of T2|C` by A10,A96,XBOOLE_1:1; A98: P2 c= Component_of Down(x,C`) by A10,A96; A99: P2 misses C by A53,SUBSET_1:23; then A100: P2 misses Jc by A4,XBOOLE_1:7,63; A101: P2 misses Jd by A4,A99,XBOOLE_1:7,63; A102: x`1 = 1/2*((k+l)`1) by TOPREAL3:4 .= 1/2*(k`1+l`1) by TOPREAL3:2 .= 0 by A22,A44; then A103: LSeg(d,x) is vertical by Lm22,SPPOL_1:16; A104: x = |[x`1,x`2]| by EUCLID:53; A105: x`2 < l`2 by A62,Th3; A106: k`2 < x`2 by A62,Th2; then A107: d`2 <= x`2 by A1,A18,A41,Lm23,Th84,XXREAL_0:2; d`1 = d`1; then A108: LSeg(d,x) c= LSeg(d,l) by A33,A103,A105,A107,GOBOARD7:63; A109: LSeg(d,x) misses Jc proof assume not thesis; then consider q being object such that A110: q in LSeg(d,x) and A111: q in Jc by XBOOLE_0:3; reconsider q as Point of T2 by A110; q`2 <= x`2 by A58,A102,A104,A107,A110,Lm22,JGRAPH_6:1; then A112: q`2 < l`2 by A105,XXREAL_0:2; q`1 = 0 by A33,A43,A108,A110,Lm22; then q in Vertical_Line w by A12,A13,JORDAN6:31; then q in Jc /\ Vertical_Line w by A111,XBOOLE_0:def 4; hence contradiction by A8,A9,A112,JORDAN21:29; end; set n = First_Point(P1,x,u,dR); A113: not u in R by A91,A92; A114: Fr R = dR by Th52; u in P1 by A97,TOPREAL1:1; then A115: P1 \ R <> {}T2 by A113,XBOOLE_0:def 5; x in P1 by A97,TOPREAL1:1; then P1 meets R by A51,A83,XBOOLE_0:3; then A116: P1 meets dR by A97,A114,A115,CONNSP_1:22,JORDAN6:10; P1 is closed by A95,JORDAN6:11,TOPREAL4:2; then A117: n in P1 /\ dR by A97,A116,JORDAN5C:def 1; then A118: n in dR by XBOOLE_0:def 4; A119: n in P1 by A117,XBOOLE_0:def 4; set alpha = Segment(P1,x,u,x,n); A120: rd < k`2 by A1,A18,A41,Th84; l`2 <= m`2 by A36,JORDAN21:28; then x`2 < m`2 by A105,XXREAL_0:2; then not x in dR by A21,A102,A104,A106,A120,Lm86; then A121: alpha is_an_arc_of x,n by A95,A118,A119,JORDAN16:24,TOPREAL4:2; A122: alpha misses Jc by A100,JORDAN16:2,XBOOLE_1:63; A123: alpha misses Jd by A101,JORDAN16:2,XBOOLE_1:63; consider Pdx being Path of d,x, fdx being Function of I[01], T2|LSeg(d,x) such that A124: rng fdx = LSeg(d,x) and A125: Pdx = fdx by Th43; consider PJc being Path of a,b, fJc being Function of I[01], T2|Jc such that A126: rng fJc = Jc and A127: PJc = fJc by A2,Th42; consider PJd being Path of a,b, fJd being Function of I[01], T2|Jd such that A128: rng fJd = Jd and A129: PJd = fJd by A3,Th42; consider Palpha being Path of x,n, falpha being Function of I[01], T2|alpha such that A130: rng falpha = alpha and A131: Palpha = falpha by A121,Th42; n in R by A118,Lm67; then A132: ex p st p = n & rl <= p`1 & p`1 <= rp & rd <= p`2 & p`2 <= rg; rng PJc c= the carrier of TR by A11,A19,A84,A126,A127; then reconsider h = PJc as Path of AR,BR by Th30; rng PJd c= the carrier of TR by A11,A18,A84,A128,A129; then reconsider H = PJd as Path of AR,BR by Th30; A133: LSeg(d,x) c= R by A51,A83,Lm63,Lm67,JORDAN1:def 1; A134: alpha c= R by A51,A83,A95,A113,Th57,TOPREAL4:2; A135: ld in LSeg(ld,lg) by RLTOPSP1:68; A136: pd in LSeg(pd,pg) by RLTOPSP1:68; LSeg(lg,c) misses C by A1,Lm78; then A137: LSeg(lg,c) misses Jc by A4,XBOOLE_1:7,63; A138: LSeg(lg,c) c= R by Lm67,Lm70; A139: LSeg(pg,c) c= R by Lm67,Lm71; LSeg(pg,c) misses C by A1,Lm79; then A140: LSeg(pg,c) misses Jc by A4,XBOOLE_1:7,63; consider Plx being Path of l,x, flx being Function of I[01], T2|LSeg(l,x) such that A141: rng flx = LSeg(l,x) and A142: Plx = flx by Th43; set PCX = Pcm + Pml + Plx; A143: rng PCX = rng Pcm \/ rng Pml \/ rng Plx by Th40; A144: ml misses Jd proof assume ml meets Jd; then consider q being object such that A145: q in ml and A146: q in Jd by XBOOLE_0:3; q in {a,b} by A5,A29,A145,A146,XBOOLE_0:def 4; hence contradiction by A30,A145,XBOOLE_0:3; end; A147: LSeg(c,m) /\ C = {m} by A1,Th91; A148: LSeg(c,m) misses Jd proof assume LSeg(c,m) meets Jd; then consider q being object such that A149: q in LSeg(c,m) and A150: q in Jd by XBOOLE_0:3; q in {m} by A18,A147,A149,A150,XBOOLE_0:def 4; then q = m by TARSKI:def 1; then m in {a,b} by A5,A6,A150,XBOOLE_0:def 4; hence contradiction by A25,A26,TARSKI:def 2; end; LSeg(l,x) is vertical by A22,A102,SPPOL_1:16; then A151: LSeg(l,x) c= LSeg(l,k) by A44,A54,A102,A105,A106,GOBOARD7:63; l in LSeg(l,x) by RLTOPSP1:68; then {l} c= LSeg(l,x) by ZFMISC_1:31; then A152: LSeg(l,x) = LSeg(l,x) \ {l} \/ {l} by XBOOLE_1:45; LSeg(l,x) \ {l} c= LSeg(l,k) \ {l,k} proof let q be object; assume A153: q in LSeg(l,x) \ {l}; then A154: q in LSeg(l,x) by ZFMISC_1:56; A155: q <> l by A153,ZFMISC_1:56; q <> k by A22,A56,A102,A104,A105,A106,A154,JGRAPH_6:1; then not q in {l,k} by A155,TARSKI:def 2; hence thesis by A151,A154,XBOOLE_0:def 5; end; then LSeg(l,x) \ {l} c= C` by A64; then LSeg(l,x) \ {l} misses C by SUBSET_1:23; then A156: LSeg(l,x) \ {l} misses Jd by A4,XBOOLE_1:7,63; {l} misses Jd proof assume {l} meets Jd; then l in Jd by ZFMISC_1:50; then l in {a,b} by A5,A17,XBOOLE_0:def 4; hence thesis by A27,A28,TARSKI:def 2; end; then LSeg(l,x) misses Jd by A152,A156,XBOOLE_1:70; then A157: rng PCX misses Jd by A85,A86,A141,A142,A143,A144,A148,XBOOLE_1:114; LSeg(l,x) c= R by A83,A151; then A158: rng PCX c= R by A85,A86,A87,A88,A141,A142,A143,Lm1; LSeg(ld,d) misses C by A1,Lm80; then A159: LSeg(ld,d) misses Jd by A4,XBOOLE_1:7,63; LSeg(pd,d) misses C by A1,Lm81; then A160: LSeg(pd,d) misses Jd by A4,XBOOLE_1:7,63; per cases; suppose A161: n`2 < 0; per cases by A118,A161,Lm77; suppose A162: n in LSeg(a,ld); consider Pnld being Path of n,ld, fnld being Function of I[01], T2|LSeg(n,ld) such that A163: rng fnld = LSeg(n,ld) and A164: Pnld = fnld by Th43; consider Pldd being Path of ld,d, fldd being Function of I[01], T2|LSeg(ld,d) such that A165: rng fldd = LSeg(ld,d) and A166: Pldd = fldd by Th43; A167: ld`1 = n`1 by A135,A162,Lm45,Lm58; then LSeg(n,ld) is vertical by SPPOL_1:16; then LSeg(n,ld) c= LSeg(ld,lg) by A132,A167,Lm25,Lm27,Lm45,GOBOARD7:63; then A168: LSeg(n,ld) c= dR by Lm38; set K1 = PCX + Palpha + Pnld + Pldd; LSeg(n,ld) misses C by A1,A53,A98,A119,A162,Lm84; then A169: LSeg(n,ld) misses Jd by A4,XBOOLE_1:7,63; A170: rng K1 = rng PCX \/ rng Palpha \/ rng Pnld \/ rng Pldd by Lm9; then A171: rng PJd misses rng K1 by A123,A128,A129,A130,A131,A157,A159,A163,A164 ,A165,A166,A169,Lm3; A172: LSeg(ld,d) c= R by Lm67,Lm74; LSeg(n,ld) c= R by A168,Lm67; then rng K1 c= the carrier of TR by A84,A130,A131,A134,A158,A163,A164,A165,A166,A170,A172,Lm2; then reconsider v = K1 as Path of CR,DR by Th30; consider s, t being Point of I[01] such that A173: H.s = v.t by Lm16,Lm17,Lm21,Lm23,JGRAPH_8:6; A174: dom H = the carrier of I[01] by FUNCT_2:def 1; A175: dom v = the carrier of I[01] by FUNCT_2:def 1; A176: H.s in rng PJd by A174,FUNCT_1:def 3; v.t in rng K1 by A175,FUNCT_1:def 3; hence contradiction by A171,A173,A176,XBOOLE_0:3; end; suppose A177: n in LSeg(ld,d); consider Pnd being Path of n,d, fnd being Function of I[01], T2|LSeg(n,d) such that A178: rng fnd = LSeg(n,d) and A179: Pnd = fnd by Th43; set K1 = PCX + Palpha + Pnd; ld in LSeg(ld,d) by RLTOPSP1:68; then A180: ld`2 = n`2 by A177,Lm51; then A181: LSeg(n,d) is horizontal by Lm23,Lm27,SPPOL_1:15; A182: ld`1 <= n`1 by A177,Lm26,JGRAPH_6:3; n`1 <= d`1 by A177,Lm22,JGRAPH_6:3; then A183: LSeg(n,d) c= LSeg(ld,d) by A180,A181,A182,Lm51,GOBOARD7:64; then A184: LSeg(n,d) c= dR by Lm74; LSeg(n,d) misses C by A1,A183,Lm80,XBOOLE_1:63; then A185: LSeg(n,d) misses Jd by A4,XBOOLE_1:7,63; A186: rng K1 = rng PCX \/ rng Palpha \/ rng Pnd by Th40; then A187: rng K1 misses Jd by A123,A130,A131,A157,A178,A179,A185,XBOOLE_1:114; LSeg(n,d) c= R by A184,Lm67; then rng K1 c= the carrier of TR by A84,A130,A131,A134,A158,A178,A179 ,A186,Lm1; then reconsider v = K1 as Path of CR,DR by Th30; consider s, t being Point of I[01] such that A188: H.s = v.t by Lm16,Lm17,Lm21,Lm23,JGRAPH_8:6; A189: dom H = the carrier of I[01] by FUNCT_2:def 1; A190: dom v = the carrier of I[01] by FUNCT_2:def 1; A191: H.s in rng PJd by A189,FUNCT_1:def 3; v.t in rng K1 by A190,FUNCT_1:def 3; hence contradiction by A128,A129,A187,A188,A191,XBOOLE_0:3; end; suppose A192: n in LSeg(d,pd); consider Pnd being Path of n,d, fnd being Function of I[01], T2|LSeg(n,d) such that A193: rng fnd = LSeg(n,d) and A194: Pnd = fnd by Th43; set K1 = PCX + Palpha + Pnd; pd in LSeg(pd,d) by RLTOPSP1:68; then pd`2 = n`2 by A192,Lm52; then A195: LSeg(n,d) is horizontal by Lm23,Lm31,SPPOL_1:15; A196: d`2 = d`2; A197: d`1 <= n`1 by A192,Lm22,JGRAPH_6:3; n`1 <= pd`1 by A192,Lm30,JGRAPH_6:3; then A198: LSeg(n,d) c= LSeg(pd,d) by A195,A196,A197,Lm52,GOBOARD7:64; then A199: LSeg(n,d) c= dR by Lm75; LSeg(n,d) misses C by A1,A198,Lm81,XBOOLE_1:63; then A200: LSeg(n,d) misses Jd by A4,XBOOLE_1:7,63; A201: rng K1 = rng PCX \/ rng Palpha \/ rng Pnd by Th40; then A202: rng K1 misses Jd by A123,A130,A131,A157,A193,A194,A200,XBOOLE_1:114; LSeg(n,d) c= R by A199,Lm67; then rng K1 c= the carrier of TR by A84,A130,A131,A134,A158,A193,A194 ,A201,Lm1; then reconsider v = K1 as Path of CR,DR by Th30; consider s, t being Point of I[01] such that A203: H.s = v.t by Lm16,Lm17,Lm21,Lm23,JGRAPH_8:6; A204: dom H = the carrier of I[01] by FUNCT_2:def 1; A205: dom v = the carrier of I[01] by FUNCT_2:def 1; A206: H.s in rng PJd by A204,FUNCT_1:def 3; v.t in rng K1 by A205,FUNCT_1:def 3; hence contradiction by A128,A129,A202,A203,A206,XBOOLE_0:3; end; suppose A207: n in LSeg(pd,b); consider Pnpd being Path of n,pd, fnpd being Function of I[01], T2|LSeg(n,pd) such that A208: rng fnpd = LSeg(n,pd) and A209: Pnpd = fnpd by Th43; consider Ppdd being Path of pd,d, fpdd being Function of I[01], T2|LSeg(pd,d) such that A210: rng fpdd = LSeg(pd,d) and A211: Ppdd = fpdd by Th43; A212: pd`1 = n`1 by A136,A207,Lm46,Lm60; then LSeg(n,pd) is vertical by SPPOL_1:16; then LSeg(n,pd) c= LSeg(pd,pg) by A132,A212,Lm29,Lm31,Lm46,GOBOARD7:63; then A213: LSeg(n,pd) c= dR by Lm42; set K1 = PCX + Palpha + Pnpd + Ppdd; LSeg(n,pd) misses C by A1,A53,A98,A119,A207,Lm85; then A214: LSeg(n,pd) misses Jd by A4,XBOOLE_1:7,63; A215: rng K1 = rng PCX \/ rng Palpha \/ rng Pnpd \/ rng Ppdd by Lm9; then A216: rng PJd misses rng K1 by A123,A128,A129,A130,A131,A157,A160,A208,A209 ,A210,A211,A214,Lm3; A217: LSeg(pd,d) c= R by Lm67,Lm75; LSeg(n,pd) c= R by A213,Lm67; then rng K1 c= the carrier of TR by A84,A130,A131,A134,A158,A208,A209,A210,A211,A215,A217,Lm2; then reconsider v = K1 as Path of CR,DR by Th30; consider s, t being Point of I[01] such that A218: H.s = v.t by Lm16,Lm17,Lm21,Lm23,JGRAPH_8:6; A219: dom H = the carrier of I[01] by FUNCT_2:def 1; A220: dom v = the carrier of I[01] by FUNCT_2:def 1; A221: H.s in rng PJd by A219,FUNCT_1:def 3; v.t in rng K1 by A220,FUNCT_1:def 3; hence contradiction by A216,A218,A221,XBOOLE_0:3; end; end; suppose A222: n`2 >= 0; per cases by A118,A222,Lm76; suppose A223: n in LSeg(a,lg); consider Pnlg being Path of n,lg, fnlg being Function of I[01], T2|LSeg(n,lg) such that A224: rng fnlg = LSeg(n,lg) and A225: Pnlg = fnlg by Th43; consider Plgc being Path of lg,c, flgc being Function of I[01], T2|LSeg(lg,c) such that A226: rng flgc = LSeg(lg,c) and A227: Plgc = flgc by Th43; A228: ld`1 = n`1 by A135,A223,Lm45,Lm57; then LSeg(n,lg) is vertical by Lm24,Lm26,SPPOL_1:16; then LSeg(n,lg) c= LSeg(ld,lg) by A132,A228,Lm25,Lm27,Lm45,GOBOARD7:63; then A229: LSeg(n,lg) c= dR by Lm38; set K1 = Pdx + Palpha + Pnlg + Plgc; LSeg(n,lg) misses C by A1,A53,A98,A119,A223,Lm82; then A230: LSeg(n,lg) misses Jc by A4,XBOOLE_1:7,63; A231: rng K1 = rng Pdx \/ rng Palpha \/ rng Pnlg \/ rng Plgc by Lm9; then A232: rng K1 misses Jc by A109,A122,A124,A125,A130,A131,A137,A224,A225,A226 ,A227,A230,Lm3; A233: rng K1 = rng -K1 by Th32; LSeg(n,lg) c= R by A229,Lm67; then rng K1 c= the carrier of TR by A84,A124,A125,A130,A131,A133,A134,A138,A224,A225,A226,A227,A231,Lm2; then reconsider v = -K1 as Path of CR,DR by A233,Th30; consider s, t being Point of I[01] such that A234: h.s = v.t by Lm16,Lm17,Lm21,Lm23,JGRAPH_8:6; A235: dom h = the carrier of I[01] by FUNCT_2:def 1; A236: dom v = the carrier of I[01] by FUNCT_2:def 1; A237: h.s in rng PJc by A235,FUNCT_1:def 3; v.t in rng -K1 by A236,FUNCT_1:def 3; hence contradiction by A126,A127,A232,A233,A234,A237,XBOOLE_0:3; end; suppose A238: n in LSeg(lg,c); consider Pnc being Path of n,c, fnc being Function of I[01], T2|LSeg(n,c) such that A239: rng fnc = LSeg(n,c) and A240: Pnc = fnc by Th43; set K1 = Pdx + Palpha + Pnc; lg in LSeg(lg,c) by RLTOPSP1:68; then A241: lg`2 = n`2 by A238,Lm53; then A242: LSeg(n,c) is horizontal by Lm21,Lm25,SPPOL_1:15; A243: lg`1 <= n`1 by A238,Lm24,JGRAPH_6:3; n`1 <= c`1 by A238,Lm20,JGRAPH_6:3; then A244: LSeg(n,c) c= LSeg(lg,c) by A241,A242,A243,Lm53,GOBOARD7:64; then A245: LSeg(n,c) c= dR by Lm70; LSeg(n,c) misses C by A1,A244,Lm78,XBOOLE_1:63; then A246: LSeg(n,c) misses Jc by A4,XBOOLE_1:7,63; A247: rng K1 = rng Pdx \/ rng Palpha \/ rng Pnc by Th40; then A248: rng K1 misses Jc by A109,A122,A124,A125,A130,A131,A239,A240,A246, XBOOLE_1:114; A249: rng K1 = rng -K1 by Th32; LSeg(n,c) c= R by A245,Lm67; then rng K1 c= the carrier of TR by A84,A124,A125,A130,A131,A133,A134,A239,A240,A247,Lm1; then reconsider v = -K1 as Path of CR,DR by A249,Th30; consider s, t being Point of I[01] such that A250: h.s = v.t by Lm16,Lm17,Lm21,Lm23,JGRAPH_8:6; A251: dom h = the carrier of I[01] by FUNCT_2:def 1; A252: dom v = the carrier of I[01] by FUNCT_2:def 1; A253: h.s in rng PJc by A251,FUNCT_1:def 3; v.t in rng -K1 by A252,FUNCT_1:def 3; hence contradiction by A126,A127,A248,A249,A250,A253,XBOOLE_0:3; end; suppose A254: n in LSeg(c,pg); consider Pnc being Path of n,c, fnc being Function of I[01], T2|LSeg(n,c) such that A255: rng fnc = LSeg(n,c) and A256: Pnc = fnc by Th43; set K1 = Pdx + Palpha + Pnc; pg in LSeg(pg,c) by RLTOPSP1:68; then pg`2 = n`2 by A254,Lm54; then A257: LSeg(n,c) is horizontal by Lm21,Lm29,SPPOL_1:15; A258: c`2 = c`2; A259: c`1 <= n`1 by A254,Lm20,JGRAPH_6:3; n`1 <= pg`1 by A254,Lm28,JGRAPH_6:3; then A260: LSeg(c,n) c= LSeg(c,pg) by A257,A258,A259,Lm54,GOBOARD7:64; then A261: LSeg(n,c) c= dR by Lm71; LSeg(n,c) misses C by A1,A260,Lm79,XBOOLE_1:63; then A262: LSeg(n,c) misses Jc by A4,XBOOLE_1:7,63; A263: rng K1 = rng Pdx \/ rng Palpha \/ rng Pnc by Th40; then A264: rng K1 misses Jc by A109,A122,A124,A125,A130,A131,A255,A256,A262, XBOOLE_1:114; A265: rng K1 = rng -K1 by Th32; LSeg(n,c) c= R by A261,Lm67; then rng K1 c= the carrier of TR by A84,A124,A125,A130,A131,A133,A134,A255,A256,A263,Lm1; then reconsider v = -K1 as Path of CR,DR by A265,Th30; consider s, t being Point of I[01] such that A266: h.s = v.t by Lm16,Lm17,Lm21,Lm23,JGRAPH_8:6; A267: dom h = the carrier of I[01] by FUNCT_2:def 1; A268: dom v = the carrier of I[01] by FUNCT_2:def 1; A269: h.s in rng PJc by A267,FUNCT_1:def 3; v.t in rng -K1 by A268,FUNCT_1:def 3; hence contradiction by A126,A127,A264,A265,A266,A269,XBOOLE_0:3; end; suppose A270: n in LSeg(pg,b); consider Pnpg being Path of n,pg, fnpg being Function of I[01], T2|LSeg(n,pg) such that A271: rng fnpg = LSeg(n,pg) and A272: Pnpg = fnpg by Th43; consider Ppgc being Path of pg,c, fpgc being Function of I[01], T2|LSeg(pg,c) such that A273: rng fpgc = LSeg(pg,c) and A274: Ppgc = fpgc by Th43; A275: pd`1 = n`1 by A136,A270,Lm46,Lm59; then LSeg(n,pg) is vertical by Lm28,Lm30,SPPOL_1:16; then LSeg(n,pg) c= LSeg(pd,pg) by A132,A275,Lm29,Lm31,Lm46,GOBOARD7:63; then A276: LSeg(n,pg) c= dR by Lm42; set K1 = Pdx + Palpha + Pnpg + Ppgc; LSeg(n,pg) misses C by A1,A53,A98,A119,A270,Lm83; then A277: LSeg(n,pg) misses Jc by A4,XBOOLE_1:7,63; A278: rng K1 = rng Pdx \/ rng Palpha \/ rng Pnpg \/ rng Ppgc by Lm9; then A279: rng K1 misses Jc by A109,A122,A124,A125,A130,A131,A140,A271,A272,A273 ,A274,A277,Lm3; A280: rng K1 = rng -K1 by Th32; LSeg(n,pg) c= R by A276,Lm67; then rng K1 c= the carrier of TR by A84,A124,A125,A130,A131,A133,A134,A139,A271,A272,A273,A274,A278,Lm2; then reconsider v = -K1 as Path of CR,DR by A280,Th30; consider s, t being Point of I[01] such that A281: h.s = v.t by Lm16,Lm17,Lm21,Lm23,JGRAPH_8:6; A282: dom h = the carrier of I[01] by FUNCT_2:def 1; A283: dom v = the carrier of I[01] by FUNCT_2:def 1; A284: h.s in rng PJc by A282,FUNCT_1:def 3; v.t in rng -K1 by A283,FUNCT_1:def 3; hence contradiction by A126,A127,A279,A280,A281,A284,XBOOLE_0:3; end; end; end; :: uniqueness let V be Subset of T2; assume A285: V is_inside_component_of C; assume A286: V <> Ux; consider VP being Subset of T2|C` such that A287: VP = V and A288: VP is a_component and VP is bounded Subset of Euclid 2 by A285,JORDAN2C:13; reconsider T2C = T2|C` as non empty SubSpace of T2; VP <> {}(T2|C`) by A288,CONNSP_1:32; then reconsider VP as non empty Subset of T2C; A289: V misses C by A53,A287,SUBSET_1:23; consider Pjd being Path of j,d, fjd being Function of I[01], T2|LSeg(j,d) such that A290: rng fjd = LSeg(j,d) and A291: Pjd = fjd by Th43; consider Plk being Path of l,k, flk being Function of I[01], T2|LSeg(l,k) such that A292: rng flk = LSeg(l,k) and A293: Plk = flk by Th43; set beta = Pcm + Pml + Plk + Pkj + Pjd; A294: rng beta = rng Pcm \/ rng Pml \/ rng Plk \/ rng Pkj \/ rng Pjd by Lm11; dom beta = [#]I[01] by FUNCT_2:def 1; then beta.:dom beta is compact by WEIERSTR:8; then A295: rng beta is closed by RELAT_1:113; A296: ml misses V by A19,A29,A289,XBOOLE_1:1,63; {l,k} c= LSeg(l,k) proof let x be object; assume x in {l,k}; then x = l or x = k by TARSKI:def 2; hence thesis by RLTOPSP1:68; end; then A297: LSeg(l,k) = LSeg(l,k) \ {l,k} \/ {l,k} by XBOOLE_1:45; A298: LSeg(l,k) \ {l,k} misses V proof assume not thesis; then ex q being object st ( q in LSeg(l,k) \ {l,k})&( q in V) by XBOOLE_0:3; then V meets Ux by A10,A82,XBOOLE_0:3; hence contradiction by A10,A52,A286,A287,A288,CONNSP_1:35; end; A299: not l in V by A17,A19,A289,XBOOLE_0:3; not k in V by A18,A41,A289,XBOOLE_0:3; then {l,k} misses V by A299,ZFMISC_1:51; then A300: LSeg(l,k) misses V by A297,A298,XBOOLE_1:70; A301: kj misses V by A50,A289,XBOOLE_1:63; A302: LSeg(j,d) misses V by A1,A285,Th90; LSeg(c,m) misses V by A1,A285,Th89; then LSeg(c,m) \/ ml \/ LSeg(l,k) misses V by A296,A300,XBOOLE_1:114; then A303: rng beta misses V by A85,A86,A290,A291,A292,A293,A294,A301,A302, XBOOLE_1:114; A304: m = |[m`1,m`2]| by EUCLID:53; A305: c = |[c`1,c`2]| by EUCLID:53; A306: j = |[j`1,j`2]| by EUCLID:53; A307: not a in LSeg(c,m) by A12,A13,A21,A23,A24,A304,A305,Lm16,JGRAPH_6:1; not a in ml by A30,ZFMISC_1:49; then A308: not a in LSeg(c,m) \/ ml by A307,XBOOLE_0:def 3; not a in LSeg(l,k) by A22,A44,A56,A57,A59,Lm16,JGRAPH_6:1; then A309: not a in LSeg(c,m) \/ ml \/ LSeg(l,k) by A308,XBOOLE_0:def 3; not a in kj by A49,ZFMISC_1:49; then A310: not a in LSeg(c,m) \/ ml \/ LSeg(l,k) \/ kj by A309,XBOOLE_0:def 3; not a in LSeg(j,d) by A34,A35,A58,A306,Lm16,Lm22,JGRAPH_6:1; then not a in rng beta by A85,A86,A290,A291,A292,A293,A294,A310, XBOOLE_0:def 3; then consider ra being positive Real such that A311: Ball(a,ra) misses rng beta by A295,Th25; A312: not b in LSeg(c,m) by A12,A13,A21,A23,A24,A304,A305,Lm17,JGRAPH_6:1; not b in ml by A30,ZFMISC_1:49; then A313: not b in LSeg(c,m) \/ ml by A312,XBOOLE_0:def 3; not b in LSeg(l,k) by A22,A44,A56,A57,A59,Lm17,JGRAPH_6:1; then A314: not b in LSeg(c,m) \/ ml \/ LSeg(l,k) by A313,XBOOLE_0:def 3; not b in kj by A49,ZFMISC_1:49; then A315: not b in LSeg(c,m) \/ ml \/ LSeg(l,k) \/ kj by A314,XBOOLE_0:def 3; not b in LSeg(j,d) by A34,A35,A58,A306,Lm17,Lm22,JGRAPH_6:1; then not b in rng beta by A85,A86,A290,A291,A292,A293,A294,A315, XBOOLE_0:def 3; then consider rb being positive Real such that A316: Ball(b,rb) misses rng beta by A295,Th25; set A = Ball(a,ra), B = Ball(b,rb); A317: a in A by Th16; A318: b in B by Th16; VP is non empty; then consider t being object such that A319: t in V by A287; V in {W where W is Subset of T2: W is_inside_component_of C} by A285; then t in BDD C by A319,TARSKI:def 4; then A320: C = Fr V by A287,A288,Lm15; then a in Cl V by A14,XBOOLE_0:def 4; then A meets V by A317,PRE_TOPC:def 7; then consider u being object such that A321: u in A and A322: u in V by XBOOLE_0:3; b in Cl V by A15,A320,XBOOLE_0:def 4; then B meets V by A318,PRE_TOPC:def 7; then consider v being object such that A323: v in B and A324: v in V by XBOOLE_0:3; reconsider u, v as Point of T2 by A321,A323; A325: the carrier of T2C|VP = VP by PRE_TOPC:8; reconsider u1 = u, v1 = v as Point of T2C|VP by A287,A322,A324,PRE_TOPC:8; T2C|VP is pathwise_connected by A288,Th69; then A326: u1,v1 are_connected; then consider fuv being Function of I[01], T2C|VP such that A327: fuv is continuous and A328: fuv.0 = u1 and A329: fuv.1 = v1; A330: T2C|VP = T2|V by A287,GOBOARD9:2; fuv is Path of u1,v1 by A326,A327,A328,A329,BORSUK_2:def 2; then reconsider uv = fuv as Path of u,v by A326,A330,TOPALG_2:1; A331: rng fuv c= the carrier of T2C|VP; then A332: rng uv misses rng beta by A287,A303,A325,XBOOLE_1:63; consider au being Path of a,u, fau being Function of I[01], T2|LSeg(a,u) such that A333: rng fau = LSeg(a,u) and A334: au = fau by Th43; consider vb being Path of v,b, fvb being Function of I[01], T2|LSeg(v,b) such that A335: rng fvb = LSeg(v,b) and A336: vb = fvb by Th43; set AB = au + uv + vb; A337: rng AB = rng au \/ rng uv \/ rng vb by Th40; a in A by Th16; then LSeg(a,u) c= A by A321,JORDAN1:def 1; then A338: LSeg(a,u) misses rng beta by A311,XBOOLE_1:63; b in B by Th16; then LSeg(v,b) c= B by A323,JORDAN1:def 1; then LSeg(v,b) misses rng beta by A316,XBOOLE_1:63; then A339: rng AB misses rng beta by A332,A333,A334,A335,A336,A337,A338,XBOOLE_1:114 ; A340: a,b are_connected by BORSUK_2:def 3; A341: V c= R by A1,A285,Th93; then A342: LSeg(a,u) c= R by A11,A14,A322,JORDAN1:def 1; A343: LSeg(v,b) c= R by A11,A15,A324,A341,JORDAN1:def 1; rng uv c= R by A287,A325,A331,A341; then LSeg(a,u) \/ rng uv c= R by A342,XBOOLE_1:8; then rng AB c= the carrier of TR by A84,A333,A334,A335,A336,A337,A343, XBOOLE_1:8; then reconsider h = AB as Path of AR,BR by A340,Th29; A344: c,d are_connected by BORSUK_2:def 3; LSeg(c,m) \/ ml c= R by A87,A88,XBOOLE_1:8; then A345: LSeg(c,m) \/ ml \/ LSeg(l,k) c= R by A83,XBOOLE_1:8; kj c= R by A11,A50; then A346: LSeg(c,m) \/ ml \/ LSeg(l,k) \/ kj c= R by A345,XBOOLE_1:8; LSeg(j,d) c= R by A11,A32,Lm63,Lm67,JORDAN1:def 1; then rng beta c= the carrier of TR by A84,A85,A86,A290,A291,A292,A293,A294 ,A346,XBOOLE_1:8; then reconsider v = beta as Path of CR,DR by A344,Th29; consider s, t being Point of I[01] such that A347: h.s = v.t by Lm16,Lm17,Lm21,Lm23,JGRAPH_8:6; A348: dom h = the carrier of I[01] by FUNCT_2:def 1; A349: dom v = the carrier of I[01] by FUNCT_2:def 1; A350: h.s in rng AB by A348,FUNCT_1:def 3; v.t in rng beta by A349,FUNCT_1:def 3; hence contradiction by A339,A347,A350,XBOOLE_0:3; end; theorem Th96: |[-1,0]|,|[1,0]| realize-max-dist-in C implies for Jc, Jd being compact with_the_max_arc Subset of TOP-REAL 2 st Jc is_an_arc_of |[-1,0]|,|[1,0]| & Jd is_an_arc_of |[-1,0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[-1,0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc holds BDD C = Component_of Down ((1/2) * ((UMP (LSeg(LMP Jc,|[0,-3]|) /\ Jd)) + LMP Jc), C`) proof assume A1: a,b realize-max-dist-in C; let Jc, Jd being compact with_the_max_arc Subset of T2 such that A2: Jc is_an_arc_of a,b and A3: Jd is_an_arc_of a,b and A4: C = Jc \/ Jd and A5: Jc /\ Jd = {a,b} and A6: UMP C in Jc and A7: LMP C in Jd and A8: W-bound C = W-bound Jc and A9: E-bound C = E-bound Jc; reconsider Ux = Component_of Down((1/2) * ((UMP (LSeg(LMP Jc,d) /\ Jd)) + LMP Jc),C`) as Subset of T2 by PRE_TOPC:11; Ux = BDD C proof Ux is_inside_component_of C by A1,A2,A3,A4,A5,A6,A7,A8,A9,Th95; hence Ux c= BDD C by JORDAN2C:22; set F = {B where B is Subset of T2: B is_inside_component_of C}; let q be object; assume q in BDD C; then consider Z being set such that A10: q in Z and A11: Z in F by TARSKI:def 4; ex B being Subset of T2 st Z = B & B is_inside_component_of C by A11; hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,Th95; end; hence thesis; end; Lm91: |[-1,0]|,|[1,0]| realize-max-dist-in C implies C is Jordan proof assume A1: a,b realize-max-dist-in C; then consider Jc, Jd being compact with_the_max_arc Subset of T2 such that A2: Jc is_an_arc_of a,b and A3: Jd is_an_arc_of a,b and A4: C = Jc \/ Jd and A5: Jc /\ Jd = {a,b} and A6: UMP C in Jc and A7: LMP C in Jd and A8: W-bound C = W-bound Jc and A9: E-bound C = E-bound Jc by Lm90; set l = LMP Jc; set LJ = LSeg(l,d) /\ Jd; set k = UMP LJ; set x = (1/2)*(k+l); A10: Component_of Down(x,C`) is a_component by CONNSP_1:40; A11: Component_of Down(x,C`) = BDD C by A1,A2,A3,A4,A5,A6,A7,A8,A9,Th96; thus C` <> {}; take A1 = UBD C, A2 = BDD C; thus C` = A1 \/ A2 by JORDAN2C:27; thus A1 misses A2 by JORDAN2C:24; A12: Component_of Down(x,C`) <> {}(T2|C`) by A10,CONNSP_1:32; A1 is_a_component_of C` by JORDAN2C:124; then A13: ex B1 being Subset of T2|C` st B1 = A1 & B1 is a_component; then A14: C = Fr A1 by A11,A12,Lm15 .= Cl A1 /\ Cl A1`; A15: C = Fr A2 by A10,A11,A12,Lm15 .= Cl A2 /\ Cl A2`; A2 c= C` by JORDAN2C:25; then C misses A2 by SUBSET_1:23; then A16: C c= Cl A2 \ A2 by A15,XBOOLE_1:17,86; A17: A1 misses A2 by JORDAN2C:24; then A2 c= A1` by SUBSET_1:23; then A18: Cl A2 c= A1` by TOPS_1:5; A1 \/ A2 = C` by JORDAN2C:27; then A1 \/ A2 misses C by SUBSET_1:23; then C misses A1 by XBOOLE_1:70; then A19: A2 \/ C misses A1 by A17,XBOOLE_1:70; A2 \/ A1 = C` by JORDAN2C:27; then (A2 \/ A1)` misses C` by SUBSET_1:23; then (A2 \/ A1)` /\ C` = {}; then (A2 \/ A1 \/ C)` = {} by XBOOLE_1:53; then ((A2 \/ C) \/ A1)` = {} by XBOOLE_1:4; then (A2 \/ C)` /\ A1` = {} by XBOOLE_1:53; then (A2 \/ C)` misses A1`; then Cl A2 c= A2 \/ C by A18,A19,SUBSET_1:25; then A20: Cl A2 \ A2 c= C by XBOOLE_1:43; A1 c= C` by JORDAN2C:26; then C misses A1 by SUBSET_1:23; then A21: C c= Cl A1 \ A1 by A14,XBOOLE_1:17,86; A1 c= A2` by A17,SUBSET_1:23; then A22: Cl A1 c= A2` by TOPS_1:5; A2 \/ A1 = C` by JORDAN2C:27; then A2 \/ A1 misses C by SUBSET_1:23; then C misses A2 by XBOOLE_1:70; then A23: A1 \/ C misses A2 by A17,XBOOLE_1:70; A1 \/ A2 = C` by JORDAN2C:27; then (A1 \/ A2)` misses C` by SUBSET_1:23; then (A1 \/ A2)` /\ C` = {}; then (A1 \/ A2 \/ C)` = {} by XBOOLE_1:53; then ((A1 \/ C) \/ A2)` = {} by XBOOLE_1:4; then (A1 \/ C)` /\ A2` = {} by XBOOLE_1:53; then (A1 \/ C)` misses A2`; then Cl A1 c= A1 \/ C by A22,A23,SUBSET_1:25; then Cl A1 \ A1 c= C by XBOOLE_1:43; hence (Cl A1) \ A1 = C by A21 .= (Cl A2) \ A2 by A16,A20; thus thesis by A11,A13,CONNSP_1:40; end; Lm92: C is Jordan proof consider f being Homeomorphism of T2 such that A1: a,b realize-max-dist-in f.:C by JORDAN24:7; A2: f" is Homeomorphism of T2 by TOPGRP_1:30; f.:C is Simple_closed_curve by Th70; then f.:C is Jordan by A1,Lm91; then A3: f".:(f.:C) is Jordan by A2,JORDAN24:16; A4: f" = f qua Function" by TOPS_2:def 4; dom f = the carrier of T2 by FUNCT_2:def 1; hence thesis by A3,A4,FUNCT_1:107; end; registration :: do not remove it let C; cluster BDD C -> non empty; coherence proof C is Jordan by Lm92; then BDD C is_inside_component_of C by JORDAN2C:108; then BDD C is_a_component_of C`; then ex B1 being Subset of T2|C` st B1 = BDD C & B1 is a_component; then BDD C <> {}(T2|C`) by CONNSP_1:32; hence thesis; end; end; theorem U = P & U is a_component implies C = Fr P proof BDD C is non empty; hence thesis by Lm15; end; theorem :: Jordan's Curve Theorem for C being Simple_closed_curve ex A1, A2 being Subset of TOP-REAL 2 st C` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & for C1, C2 being Subset of (TOP-REAL 2)|C` st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component proof let C; C is Jordan by Lm92; hence thesis; end; ::$N Jordan Curve Theorem theorem for C being Simple_closed_curve holds C is Jordan by Lm92;