:: Jordan Curve Theorem :: by Artur Korni{\l}owicz :: :: Received September 15, 2005 :: Copyright (c) 2005-2017 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; 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; registration let M be symmetric triangle Reflexive MetrStruct, x, y be Point of M; cluster dist(x,y) -> non negative; end; registration let n be Element of NAT, x, y be Point of TOP-REAL n; cluster dist(x,y) -> non negative; end; theorem :: JORDAN:1 for p1, p2 being Point of TOP-REAL n st p1 <> p2 holds 1/2*(p1+p2) <> p1; theorem :: JORDAN:2 p1`2 < p2`2 implies p1`2 < (1/2*(p1+p2))`2; theorem :: JORDAN:3 p1`2 < p2`2 implies (1/2*(p1+p2))`2 < p2`2; theorem :: JORDAN:4 for A being vertical Subset of TOP-REAL 2 holds A /\ B is vertical; theorem :: JORDAN:5 for A being horizontal Subset of TOP-REAL 2 holds A /\ B is horizontal; theorem :: JORDAN:6 p in LSeg(p1,p2) & LSeg(p1,p2) is vertical implies LSeg(p,p2) is vertical; theorem :: JORDAN:7 p in LSeg(p1,p2) & LSeg(p1,p2) is horizontal implies LSeg(p,p2) is horizontal ; 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; cluster LSeg(NW-corner P,SW-corner P) -> vertical; cluster LSeg(NE-corner P,SE-corner P) -> vertical; end; registration let P be Subset of TOP-REAL 2; cluster LSeg(SE-corner P,SW-corner P) -> horizontal; cluster LSeg(SW-corner P,NW-corner P) -> vertical; cluster LSeg(SE-corner P,NE-corner P) -> vertical; end; registration cluster vertical non empty compact -> with_the_max_arc for Subset of TOP-REAL 2; end; theorem :: JORDAN:8 p1`1 <= r & r <= p2`1 implies LSeg(p1,p2) meets Vertical_Line(r); theorem :: JORDAN:9 p1`2 <= r & r <= p2`2 implies LSeg(p1,p2) meets Horizontal_Line(r); registration let n; cluster empty -> bounded for Subset of TOP-REAL n; cluster non bounded -> non empty for Subset of TOP-REAL n; end; registration let n be non zero Nat; cluster open closed non bounded convex for Subset of TOP-REAL n; end; theorem :: JORDAN:10 for C being compact Subset of TOP-REAL 2 holds north_halfline UMP C \ {UMP C} misses C; theorem :: JORDAN:11 for C being compact Subset of TOP-REAL 2 holds south_halfline LMP C \ {LMP C} misses C; theorem :: JORDAN:12 for C being compact Subset of TOP-REAL 2 holds north_halfline UMP C \ {UMP C} c= UBD C; theorem :: JORDAN:13 for C being compact Subset of TOP-REAL 2 holds south_halfline LMP C \ {LMP C} c= UBD C; theorem :: JORDAN:14 A is_inside_component_of B implies UBD B misses A; theorem :: JORDAN:15 A is_outside_component_of B implies BDD B misses A; theorem :: JORDAN:16 for n being Nat for r being positive Real for a being Point of TOP-REAL n holds a in Ball(a,r); theorem :: JORDAN:17 for r being non negative Real for p being Point of TOP-REAL n holds p is Point of Tdisk(p,r); 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; end; theorem :: JORDAN:18 r <= s implies Ball(x,r) c= Ball(x,s); theorem :: JORDAN:19 cl_Ball(x,r) \ Ball(x,r) = Sphere(x,r); theorem :: JORDAN:20 y in Sphere(x,r) implies LSeg(x,y) \ {x,y} c= Ball(x,r); theorem :: JORDAN:21 r < s implies cl_Ball(x,r) c= Ball(x,s); theorem :: JORDAN:22 r < s implies Sphere(x,r) c= Ball(x,s); theorem :: JORDAN:23 for r being non zero Real holds Cl Ball(x,r) = cl_Ball(x,r); theorem :: JORDAN:24 for r being non zero Real holds Fr Ball(x,r) = Sphere(x,r); registration let n be non zero Element of NAT; cluster bounded -> proper for Subset of TOP-REAL n; end; registration let n; cluster non empty closed convex bounded for Subset of TOP-REAL n; cluster non empty open convex bounded for Subset of TOP-REAL n; end; registration let n be Element of NAT; let A be bounded Subset of TOP-REAL n; cluster Cl A -> bounded; end; registration let n be Element of NAT; let A be bounded Subset of TOP-REAL n; cluster Fr A -> bounded; end; theorem :: JORDAN:25 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; theorem :: JORDAN:26 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); theorem :: JORDAN:27 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; end; registration let p, r; cluster Tdisk(p,r) -> closed; end; registration let p, r; cluster Tdisk(p,r) -> compact; end; begin :: Paths theorem :: JORDAN:28 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; theorem :: JORDAN:29 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; theorem :: JORDAN:30 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; theorem :: JORDAN:31 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; theorem :: JORDAN:32 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; theorem :: JORDAN:33 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); theorem :: JORDAN:34 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); theorem :: JORDAN:35 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); theorem :: JORDAN:36 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); theorem :: JORDAN:37 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; theorem :: JORDAN:38 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; theorem :: JORDAN:39 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; theorem :: JORDAN:40 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; theorem :: JORDAN:41 for T being non empty TopSpace, a being Point of T holds I[01] --> a is Path of a,a; theorem :: JORDAN:42 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; theorem :: JORDAN:43 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; theorem :: JORDAN:44 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}; begin :: Rectangles theorem :: JORDAN:45 a <= b & c <= d implies rectangle(a,b,c,d) c= closed_inside_of_rectangle(a,b,c,d); theorem :: JORDAN:46 inside_of_rectangle(a,b,c,d) c= closed_inside_of_rectangle(a,b,c,d); theorem :: JORDAN:47 closed_inside_of_rectangle(a,b,c,d) = outside_of_rectangle(a,b,c,d)`; registration let a, b, c, d be Real; cluster closed_inside_of_rectangle(a,b,c,d) -> closed; end; theorem :: JORDAN:48 closed_inside_of_rectangle(a,b,c,d) misses outside_of_rectangle(a,b,c,d); theorem :: JORDAN:49 closed_inside_of_rectangle(a,b,c,d) /\ inside_of_rectangle(a,b,c,d) = inside_of_rectangle(a,b,c,d); theorem :: JORDAN:50 a < b & c < d implies Int closed_inside_of_rectangle(a,b,c,d) = inside_of_rectangle(a,b,c,d); theorem :: JORDAN:51 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); theorem :: JORDAN:52 a < b & c < d implies Fr closed_inside_of_rectangle(a,b,c,d) = rectangle(a,b,c,d); theorem :: JORDAN:53 a <= b & c <= d implies W-bound closed_inside_of_rectangle(a,b,c,d) = a; theorem :: JORDAN:54 a <= b & c <= d implies S-bound closed_inside_of_rectangle(a,b,c,d) = c; theorem :: JORDAN:55 a <= b & c <= d implies E-bound closed_inside_of_rectangle(a,b,c,d) = b; theorem :: JORDAN:56 a <= b & c <= d implies N-bound closed_inside_of_rectangle(a,b,c,d) = d; theorem :: JORDAN:57 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); 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; redefine func x`2 -> Element of T; end; definition let o be Point of TOP-REAL 2; func diffX2_1(o) -> RealMap of [:TOP-REAL 2,TOP-REAL 2:] means :: JORDAN:def 1 for x being Point of [:TOP-REAL 2,TOP-REAL 2:] holds it.x = x`2`1 - o`1; func diffX2_2(o) -> RealMap of [:TOP-REAL 2,TOP-REAL 2:] means :: JORDAN:def 2 for x being Point of [:TOP-REAL 2,TOP-REAL 2:] holds it.x = x`2`2 - o`2; end; definition func diffX1_X2_1 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means :: JORDAN:def 3 for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`1`1 - x`2`1; func diffX1_X2_2 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means :: JORDAN:def 4 for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`1`2 - x`2`2; func Proj2_1 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means :: JORDAN:def 5 for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`2`1; func Proj2_2 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means :: JORDAN:def 6 for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`2`2; end; theorem :: JORDAN:58 for o being Point of TOP-REAL 2 holds diffX2_1(o) is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1; theorem :: JORDAN:59 for o being Point of TOP-REAL 2 holds diffX2_2(o) is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1; theorem :: JORDAN:60 diffX1_X2_1 is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1; theorem :: JORDAN:61 diffX1_X2_2 is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1; theorem :: JORDAN:62 Proj2_1 is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1; theorem :: JORDAN:63 Proj2_2 is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1; registration let o be Point of TOP-REAL 2; cluster diffX2_1(o) -> continuous; cluster diffX2_2(o) -> continuous; end; registration cluster diffX1_X2_1 -> continuous; cluster diffX1_X2_2 -> continuous; cluster Proj2_1 -> continuous; cluster Proj2_2 -> continuous; end; definition let n be non zero Element of NAT, o, p be Point of TOP-REAL n, r be positive Real such that p is Point of Tdisk(o,r); func DiskProj(o,r,p) -> Function of (TOP-REAL n)|(cl_Ball(o,r)\{p}), Tcircle(o,r) means :: JORDAN:def 7 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); end; theorem :: JORDAN:64 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; theorem :: JORDAN:65 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); definition let n be non zero Element of NAT, o, p be Point of TOP-REAL n, r be positive Real such that p in Ball(o,r); func RotateCircle(o,r,p) -> Function of Tcircle(o,r), Tcircle(o,r) means :: JORDAN:def 8 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); end; theorem :: JORDAN:66 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; theorem :: JORDAN:67 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; begin :: Jordan's Curve Theorem theorem :: JORDAN:68 U = P & U is a_component & V is a_component & U <> V implies Cl P misses V; theorem :: JORDAN:69 U is a_component implies (TOP-REAL 2)|C`|U is pathwise_connected; theorem :: JORDAN:70 for h being Homeomorphism of TOP-REAL 2 holds h.:C is being_simple_closed_curve; theorem :: JORDAN:71 |[-1,0]|,|[1,0]| realize-max-dist-in P implies P c= closed_inside_of_rectangle(-1,1,-3,3); theorem :: JORDAN:72 |[-1,0]|,|[1,0]| realize-max-dist-in P implies P misses LSeg(|[-1,3]|,|[1,3]|); theorem :: JORDAN:73 |[-1,0]|,|[1,0]| realize-max-dist-in P implies P misses LSeg(|[-1,-3]|,|[1,-3]|); theorem :: JORDAN:74 |[-1,0]|,|[1,0]| realize-max-dist-in P implies P /\ rectangle(-1,1,-3,3) = {|[-1,0]|,|[1,0]|}; theorem :: JORDAN:75 |[-1,0]|,|[1,0]| realize-max-dist-in P implies W-bound P = -1; theorem :: JORDAN:76 |[-1,0]|,|[1,0]| realize-max-dist-in P implies E-bound P = 1; theorem :: JORDAN:77 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]|}; theorem :: JORDAN:78 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]|}; theorem :: JORDAN:79 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]|; theorem :: JORDAN:80 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]|; theorem :: JORDAN:81 |[-1,0]|,|[1,0]| realize-max-dist-in P implies LSeg(|[0,3]|,UMP P) is vertical; theorem :: JORDAN:82 |[-1,0]|,|[1,0]| realize-max-dist-in P implies LSeg(LMP P,|[0,-3]|) is vertical; theorem :: JORDAN:83 |[-1,0]|,|[1,0]| realize-max-dist-in P & p in P implies p`2 < 3; theorem :: JORDAN:84 |[-1,0]|,|[1,0]| realize-max-dist-in P & p in P implies -3 < p`2; theorem :: JORDAN:85 |[-1,0]|,|[1,0]| realize-max-dist-in D & p in LSeg(|[0,3]|,UMP D) implies (UMP D)`2 <= p`2; theorem :: JORDAN:86 |[-1,0]|,|[1,0]| realize-max-dist-in D & p in LSeg(LMP D,|[0,-3]|) implies p`2 <= (LMP D)`2; theorem :: JORDAN:87 |[-1,0]|,|[1,0]| realize-max-dist-in D implies LSeg(|[0,3]|,UMP D) c= north_halfline UMP D; theorem :: JORDAN:88 |[-1,0]|,|[1,0]| realize-max-dist-in D implies LSeg(LMP D,|[0,-3]|) c= south_halfline LMP D; theorem :: JORDAN:89 |[-1,0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C implies LSeg(|[0,3]|,UMP C) misses P; theorem :: JORDAN:90 |[-1,0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C implies LSeg(LMP C,|[0,-3]|) misses P; theorem :: JORDAN:91 |[-1,0]|,|[1,0]| realize-max-dist-in D implies LSeg(|[0,3]|,UMP D) /\ D = {UMP D}; theorem :: JORDAN:92 |[-1,0]|,|[1,0]| realize-max-dist-in D implies LSeg(|[0,-3]|,LMP D) /\ D = {LMP D}; theorem :: JORDAN:93 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); theorem :: JORDAN:94 |[-1,0]|,|[1,0]| realize-max-dist-in C implies LSeg(|[0,3]|,|[0,-3]|) meets C ; theorem :: JORDAN:95 |[-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; theorem :: JORDAN:96 |[-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`); registration :: do not remove it let C; cluster BDD C -> non empty; end; theorem :: JORDAN:97 U = P & U is a_component implies C = Fr P; theorem :: JORDAN:98 :: 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; ::\$N Jordan Curve Theorem theorem :: JORDAN:99 for C being Simple_closed_curve holds C is Jordan;