:: JORDAN semantic presentation begin registrationlet "M" be ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); cluster (Set ($#k2_metric_1 :::"dist"::: ) "(" "x" "," "y" ")" ) -> ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x", "y" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k1_topreal6 :::"dist"::: ) "(" "x" "," "y" ")" ) -> ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ; end; theorem :: JORDAN:1 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2")) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Var "p1"))))) ; theorem :: JORDAN:2 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ))) "holds" (Bool (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: JORDAN:3 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p2")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: JORDAN:4 (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "A")) "being" ($#v2_sppol_1 :::"vertical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) "is" ($#v2_sppol_1 :::"vertical"::: ) ))) ; theorem :: JORDAN:5 (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "A")) "being" ($#v1_sppol_1 :::"horizontal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) "is" ($#v1_sppol_1 :::"horizontal"::: ) ))) ; theorem :: JORDAN:6 (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) )) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "p2")) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) )) ; theorem :: JORDAN:7 (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) "is" ($#v1_sppol_1 :::"horizontal"::: ) )) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "p2")) ")" ) "is" ($#v1_sppol_1 :::"horizontal"::: ) )) ; registrationlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) "P" ")" ) "," (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) "P" ")" ) ")" ) -> ($#v1_sppol_1 :::"horizontal"::: ) ; cluster (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) "P" ")" ) "," (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) "P" ")" ) ")" ) -> ($#v2_sppol_1 :::"vertical"::: ) ; cluster (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) "P" ")" ) "," (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) "P" ")" ) ")" ) -> ($#v2_sppol_1 :::"vertical"::: ) ; end; registrationlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) "P" ")" ) "," (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) "P" ")" ) ")" ) -> ($#v1_sppol_1 :::"horizontal"::: ) ; cluster (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) "P" ")" ) "," (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) "P" ")" ) ")" ) -> ($#v2_sppol_1 :::"vertical"::: ) ; cluster (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) "P" ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) "P" ")" ) ")" ) -> ($#v2_sppol_1 :::"vertical"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#v2_sppol_1 :::"vertical"::: ) -> ($#v1_jordan21 :::"with_the_max_arc"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))); end; theorem :: JORDAN:8 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k6_jordan6 :::"Vertical_Line"::: ) (Set (Var "r")))))) ; theorem :: JORDAN:9 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k7_jordan6 :::"Horizontal_Line"::: ) (Set (Var "r")))))) ; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v9_rltopsp1 :::"bounded"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ))); cluster ($#~v9_rltopsp1 "non" ($#v9_rltopsp1 :::"bounded"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ))); end; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); cluster ($#v4_funct_1 :::"functional"::: ) ($#v3_pre_topc :::"open"::: ) ($#v4_pre_topc :::"closed"::: ) ($#~v9_rltopsp1 "non" ($#v9_rltopsp1 :::"bounded"::: ) ) ($#v1_convex1 :::"convex"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ))); end; theorem :: JORDAN:10 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k4_topreal1 :::"north_halfline"::: ) (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C")))) ; theorem :: JORDAN:11 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k6_topreal1 :::"south_halfline"::: ) (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C")))) ; theorem :: JORDAN:12 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k4_topreal1 :::"north_halfline"::: ) (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "C"))))) ; theorem :: JORDAN:13 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k6_topreal1 :::"south_halfline"::: ) (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "C"))))) ; theorem :: JORDAN:14 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "B"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A")))) ; theorem :: JORDAN:15 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set (Var "B"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A")))) ; theorem :: JORDAN:16 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ))))) ; theorem :: JORDAN:17 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Var "p")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k2_brouwer :::"Tdisk"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ))))) ; registrationlet "r" be ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p", "q" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set (Set "(" ($#k2_topreal9 :::"cl_Ball"::: ) "(" "p" "," "r" ")" ")" ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) "q" ($#k6_domain_1 :::"}"::: ) )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: JORDAN:18 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ))))) ; theorem :: JORDAN:19 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set "(" ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: JORDAN:20 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: JORDAN:21 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ))))) ; theorem :: JORDAN:22 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ))))) ; theorem :: JORDAN:23 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: JORDAN:24 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#v9_rltopsp1 :::"bounded"::: ) -> ($#v1_subset_1 :::"proper"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ))); end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#v4_funct_1 :::"functional"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_pre_topc :::"closed"::: ) ($#v9_rltopsp1 :::"bounded"::: ) ($#v1_convex1 :::"convex"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ))); cluster ($#v4_funct_1 :::"functional"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_pre_topc :::"open"::: ) ($#v9_rltopsp1 :::"bounded"::: ) ($#v1_convex1 :::"convex"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ))); end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#v9_rltopsp1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k2_pre_topc :::"Cl"::: ) "A") -> ($#v9_rltopsp1 :::"bounded"::: ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#v9_rltopsp1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k2_tops_1 :::"Fr"::: ) "A") -> ($#v9_rltopsp1 :::"bounded"::: ) ; end; theorem :: JORDAN:25 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A"))))))) ; theorem :: JORDAN:26 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#v9_rltopsp1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "ex" (Set (Var "r")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" )))))) ; theorem :: JORDAN:27 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) ))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"T_2"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"T_2"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "T"; end; registrationlet "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_brouwer :::"Tdisk"::: ) "(" "p" "," "r" ")" ) -> ($#v1_borsuk_1 :::"closed"::: ) ; end; registrationlet "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_brouwer :::"Tdisk"::: ) "(" "p" "," "r" ")" ) -> ($#v1_compts_1 :::"compact"::: ) ; end; begin theorem :: JORDAN:28 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) "is" ($#v2_connsp_1 :::"connected"::: ) )))) ; theorem :: JORDAN:29 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x1")) "," (Set (Var "x2")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))))) "holds" (Bool "(" (Bool (Set (Var "y1")) "," (Set (Var "y2")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "f")) "is" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "y1")) "," (Set (Var "y2"))) ")" )))))) ; theorem :: JORDAN:30 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x1")) "," (Set (Var "x2")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))))) "holds" (Bool "(" (Bool (Set (Var "y1")) "," (Set (Var "y2")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "f")) "is" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "y1")) "," (Set (Var "y2"))) ")" )))))) ; theorem :: JORDAN:31 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "f")) ")" )))))) ; theorem :: JORDAN:32 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "f")) ")" )))))) ; theorem :: JORDAN:33 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "g")) ")" ))))))) ; theorem :: JORDAN:34 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "g")) ")" ))))))) ; theorem :: JORDAN:35 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) (Bool "for" (Set (Var "g")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "g")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "f")) ")" ))))))) ; theorem :: JORDAN:36 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) (Bool "for" (Set (Var "g")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "g")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "f")) ")" ))))))) ; theorem :: JORDAN:37 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "g")) ")" ))))))) ; theorem :: JORDAN:38 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "g")) ")" ))))))) ; theorem :: JORDAN:39 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) (Bool "for" (Set (Var "h")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "g")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "h")) ")" )))))))) ; theorem :: JORDAN:40 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) (Bool "for" (Set (Var "h")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "g")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "h")) ")" )))))))) ; theorem :: JORDAN:41 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k6_struct_0 :::"-->"::: ) (Set (Var "a"))) "is" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "a"))))) ; theorem :: JORDAN:42 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "p1")) "," (Set (Var "p2"))(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" )))))) ; theorem :: JORDAN:43 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "ex" (Set (Var "F")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "p1")) "," (Set (Var "p2"))(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ")" ) ")" ) "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))))) ; theorem :: JORDAN:44 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "q2")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1"))) & (Bool (Set (Var "q2")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "q1")) "," (Set (Var "q2")) "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_subset_1 :::"misses"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k7_domain_1 :::"}"::: ) )) ")" )))) ; begin theorem :: JORDAN:45 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k1_sppol_2 :::"rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ))) ; theorem :: JORDAN:46 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_jgraph_6 :::"inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ))) ; theorem :: JORDAN:47 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_jgraph_6 :::"outside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k3_subset_1 :::"`"::: ) ))) ; registrationlet "a", "b", "c", "d" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" "a" "," "b" "," "c" "," "d" ")" ) -> ($#v4_pre_topc :::"closed"::: ) ; end; theorem :: JORDAN:48 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_jgraph_6 :::"outside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ))) ; theorem :: JORDAN:49 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jgraph_6 :::"inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_jgraph_6 :::"inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ))) ; theorem :: JORDAN:50 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_jgraph_6 :::"inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ))) ; theorem :: JORDAN:51 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set (Set "(" ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_jgraph_6 :::"inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_sppol_2 :::"rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ))) ; theorem :: JORDAN:52 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_sppol_2 :::"rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ))) ; theorem :: JORDAN:53 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set "(" ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ; theorem :: JORDAN:54 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set "(" ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ; theorem :: JORDAN:55 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set "(" ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; theorem :: JORDAN:56 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set "(" ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "d")))) ; theorem :: JORDAN:57 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" )) & (Bool (Bool "not" (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ))) & (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p1")) "," (Set "(" ($#k1_jordan5c :::"First_Point"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set "(" ($#k1_sppol_2 :::"rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ")" ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ))))) ; begin definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Const "S")) "," (Set (Const "T")) ($#k2_borsuk_1 :::":]"::: ) ); :: original: :::"`1"::: redefine func "x" :::"`1"::: -> ($#m1_subset_1 :::"Element":::) "of" "S"; :: original: :::"`2"::: redefine func "x" :::"`2"::: -> ($#m1_subset_1 :::"Element":::) "of" "T"; end; definitionlet "o" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); func :::"diffX2_1"::: "o" -> ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) means :: JORDAN:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k2_jordan :::"`2"::: ) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" "o" ($#k17_euclid :::"`1"::: ) ")" )))); func :::"diffX2_2"::: "o" -> ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) means :: JORDAN:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k2_jordan :::"`2"::: ) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" "o" ($#k18_euclid :::"`2"::: ) ")" )))); end; :: deftheorem defines :::"diffX2_1"::: JORDAN:def 1 : (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_jordan :::"diffX2_1"::: ) (Set (Var "o")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k2_jordan :::"`2"::: ) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "o")) ($#k17_euclid :::"`1"::: ) ")" )))) ")" ))); :: deftheorem defines :::"diffX2_2"::: JORDAN:def 2 : (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_jordan :::"diffX2_2"::: ) (Set (Var "o")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k2_jordan :::"`2"::: ) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "o")) ($#k18_euclid :::"`2"::: ) ")" )))) ")" ))); definitionfunc :::"diffX1_X2_1"::: -> ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) means :: JORDAN:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_jordan :::"`1"::: ) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k2_jordan :::"`2"::: ) ")" ) ($#k17_euclid :::"`1"::: ) ")" )))); func :::"diffX1_X2_2"::: -> ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) means :: JORDAN:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_jordan :::"`1"::: ) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k2_jordan :::"`2"::: ) ")" ) ($#k18_euclid :::"`2"::: ) ")" )))); func :::"Proj2_1"::: -> ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) means :: JORDAN:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_jordan :::"`2"::: ) ")" ) ($#k17_euclid :::"`1"::: ) ))); func :::"Proj2_2"::: -> ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) means :: JORDAN:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_jordan :::"`2"::: ) ")" ) ($#k18_euclid :::"`2"::: ) ))); end; :: deftheorem defines :::"diffX1_X2_1"::: JORDAN:def 3 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k5_jordan :::"diffX1_X2_1"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_jordan :::"`1"::: ) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k2_jordan :::"`2"::: ) ")" ) ($#k17_euclid :::"`1"::: ) ")" )))) ")" )); :: deftheorem defines :::"diffX1_X2_2"::: JORDAN:def 4 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_jordan :::"diffX1_X2_2"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_jordan :::"`1"::: ) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k2_jordan :::"`2"::: ) ")" ) ($#k18_euclid :::"`2"::: ) ")" )))) ")" )); :: deftheorem defines :::"Proj2_1"::: JORDAN:def 5 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k7_jordan :::"Proj2_1"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_jordan :::"`2"::: ) ")" ) ($#k17_euclid :::"`1"::: ) ))) ")" )); :: deftheorem defines :::"Proj2_2"::: JORDAN:def 6 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k8_jordan :::"Proj2_2"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_jordan :::"`2"::: ) ")" ) ($#k18_euclid :::"`2"::: ) ))) ")" )); theorem :: JORDAN:58 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_jordan :::"diffX2_1"::: ) (Set (Var "o"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ))) ; theorem :: JORDAN:59 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k4_jordan :::"diffX2_2"::: ) (Set (Var "o"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ))) ; theorem :: JORDAN:60 (Bool (Set ($#k5_jordan :::"diffX1_X2_1"::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) )) ; theorem :: JORDAN:61 (Bool (Set ($#k6_jordan :::"diffX1_X2_2"::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) )) ; theorem :: JORDAN:62 (Bool (Set ($#k7_jordan :::"Proj2_1"::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) )) ; theorem :: JORDAN:63 (Bool (Set ($#k8_jordan :::"Proj2_2"::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) )) ; registrationlet "o" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k3_jordan :::"diffX2_1"::: ) "o") -> ($#v1_pscomp_1 :::"continuous"::: ) ; cluster (Set ($#k4_jordan :::"diffX2_2"::: ) "o") -> ($#v1_pscomp_1 :::"continuous"::: ) ; end; registration cluster (Set ($#k5_jordan :::"diffX1_X2_1"::: ) ) -> ($#v1_pscomp_1 :::"continuous"::: ) ; cluster (Set ($#k6_jordan :::"diffX1_X2_2"::: ) ) -> ($#v1_pscomp_1 :::"continuous"::: ) ; cluster (Set ($#k7_jordan :::"Proj2_1"::: ) ) -> ($#v1_pscomp_1 :::"continuous"::: ) ; cluster (Set ($#k8_jordan :::"Proj2_2"::: ) ) -> ($#v1_pscomp_1 :::"continuous"::: ) ; end; definitionlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "o", "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; assume (Bool (Set (Const "p")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k2_brouwer :::"Tdisk"::: ) "(" (Set (Const "o")) "," (Set (Const "r")) ")" ")" )) ; func :::"DiskProj"::: "(" "o" "," "r" "," "p" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set "(" ($#k2_topreal9 :::"cl_Ball"::: ) "(" "o" "," "r" ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) "p" ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) "," (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" "o" "," "r" ")" ")" ) means :: JORDAN:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set "(" ($#k2_topreal9 :::"cl_Ball"::: ) "(" "o" "," "r" ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) "p" ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_brouwer :::"HC"::: ) "(" "p" "," (Set (Var "y")) "," "o" "," "r" ")" )) ")" ))); end; :: deftheorem defines :::"DiskProj"::: JORDAN:def 7 : (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "o")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k2_brouwer :::"Tdisk"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ")" ))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set "(" ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) "," (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k9_jordan :::"DiskProj"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) "," (Set (Var "p")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set "(" ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_brouwer :::"HC"::: ) "(" (Set (Var "p")) "," (Set (Var "y")) "," (Set (Var "o")) "," (Set (Var "r")) ")" )) ")" ))) ")" ))))); theorem :: JORDAN:64 (Bool "for" (Set (Var "o")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k2_brouwer :::"Tdisk"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ")" ))) "holds" (Bool (Set ($#k9_jordan :::"DiskProj"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) "," (Set (Var "p")) ")" ) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; theorem :: JORDAN:65 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "o")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set "(" ($#k9_jordan :::"DiskProj"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) "," (Set (Var "p")) ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ")" )))))) ; definitionlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "o", "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; assume (Bool (Set (Const "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Const "o")) "," (Set (Const "r")) ")" )) ; func :::"RotateCircle"::: "(" "o" "," "r" "," "p" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" "o" "," "r" ")" ")" ) "," (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" "o" "," "r" ")" ")" ) means :: JORDAN:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" "o" "," "r" ")" ")" ) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_brouwer :::"HC"::: ) "(" (Set (Var "y")) "," "p" "," "o" "," "r" ")" )) ")" ))); end; :: deftheorem defines :::"RotateCircle"::: JORDAN:def 8 : (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "o")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ")" ) "," (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k10_jordan :::"RotateCircle"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) "," (Set (Var "p")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ")" ) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_brouwer :::"HC"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) "," (Set (Var "o")) "," (Set (Var "r")) ")" )) ")" ))) ")" ))))); theorem :: JORDAN:66 (Bool "for" (Set (Var "o")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set ($#k10_jordan :::"RotateCircle"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) "," (Set (Var "p")) ")" ) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; theorem :: JORDAN:67 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "o")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set ($#k10_jordan :::"RotateCircle"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) "," (Set (Var "p")) ")" ) "is" ($#v2_abian :::"without_fixpoints"::: ) )))) ; begin theorem :: JORDAN:68 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "U")) "," (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) "st" (Bool (Bool (Set (Var "U")) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Var "U")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "V")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "U")) ($#r1_hidden :::"<>"::: ) (Set (Var "V")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "V")))))) ; theorem :: JORDAN:69 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) "st" (Bool (Bool (Set (Var "U")) "is" ($#v3_connsp_1 :::"a_component"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "U"))) "is" ($#v1_borsuk_2 :::"pathwise_connected"::: ) ))) ; theorem :: JORDAN:70 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "h")) "being" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Num 2)) "holds" (Bool (Set (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set (Var "C"))) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ))) ; theorem :: JORDAN:71 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) "," (Num 3) ")" ))) ; theorem :: JORDAN:72 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 3) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 3) ($#k19_euclid :::"]|"::: ) ) ")" ))) ; theorem :: JORDAN:73 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ))) ; theorem :: JORDAN:74 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set (Var "P")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_sppol_2 :::"rectangle"::: ) "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) "," (Num 3) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k7_domain_1 :::"}"::: ) ))) ; theorem :: JORDAN:75 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) ; theorem :: JORDAN:76 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: JORDAN:77 (Bool "for" (Set (Var "P")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k14_pscomp_1 :::"W-most"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k6_domain_1 :::"}"::: ) ))) ; theorem :: JORDAN:78 (Bool "for" (Set (Var "P")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k16_pscomp_1 :::"E-most"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k6_domain_1 :::"}"::: ) ))) ; theorem :: JORDAN:79 (Bool "for" (Set (Var "P")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set ($#k19_pscomp_1 :::"W-max"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) ")" )) ; theorem :: JORDAN:80 (Bool "for" (Set (Var "P")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k23_pscomp_1 :::"E-min"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) ")" )) ; theorem :: JORDAN:81 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "P")) ")" ) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) )) ; theorem :: JORDAN:82 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "P")) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) )) ; theorem :: JORDAN:83 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 3)))) ; theorem :: JORDAN:84 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 3)) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) )))) ; theorem :: JORDAN:85 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "D")) "being" ($#v2_compts_1 :::"compact"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "D"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "D")) ")" ) ")" ))) "holds" (Bool (Set (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "D")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) )))) ; theorem :: JORDAN:86 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "D")) "being" ($#v2_compts_1 :::"compact"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "D"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "D")) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ))) "holds" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "D")) ")" ) ($#k18_euclid :::"`2"::: ) )))) ; theorem :: JORDAN:87 (Bool "for" (Set (Var "D")) "being" ($#v2_compts_1 :::"compact"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "D")) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_topreal1 :::"north_halfline"::: ) (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "D")) ")" )))) ; theorem :: JORDAN:88 (Bool "for" (Set (Var "D")) "being" ($#v2_compts_1 :::"compact"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "D")) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k6_topreal1 :::"south_halfline"::: ) (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "D")) ")" )))) ; theorem :: JORDAN:89 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "C"))) & (Bool (Set (Var "P")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C")) ")" ) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "P"))))) ; theorem :: JORDAN:90 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "C"))) & (Bool (Set (Var "P")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C")) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "P"))))) ; theorem :: JORDAN:91 (Bool "for" (Set (Var "D")) "being" ($#v2_compts_1 :::"compact"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "D")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ; theorem :: JORDAN:92 (Bool "for" (Set (Var "D")) "being" ($#v2_compts_1 :::"compact"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "D")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ; theorem :: JORDAN:93 (Bool "for" (Set (Var "P")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P"))) & (Bool (Set (Var "A")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: ) "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) "," (Num 3) ")" ))) ; theorem :: JORDAN:94 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C")))) ; theorem :: JORDAN:95 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "C")))) "holds" (Bool "for" (Set (Var "Jc")) "," (Set (Var "Jd")) "being" ($#v2_compts_1 :::"compact"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "Jc")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Var "Jd")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "Jc")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Jd")))) & (Bool (Set (Set (Var "Jc")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Jd"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "Jc"))) & (Bool (Set ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "Jd"))) & (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "Jc")))) & (Bool (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "Jc"))))) "holds" (Bool "for" (Set (Var "Ux")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "Ux")) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_1 :::"Component_of"::: ) (Set "(" ($#k2_connsp_3 :::"Down"::: ) "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set "(" (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "Jc")) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Jd")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "Jc")) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ")" )))) "holds" (Bool "(" (Bool (Set (Var "Ux")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "C"))) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "Ux"))) ")" ) ")" )))) ; theorem :: JORDAN:96 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "C")))) "holds" (Bool "for" (Set (Var "Jc")) "," (Set (Var "Jd")) "being" ($#v2_compts_1 :::"compact"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "Jc")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Var "Jd")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "Jc")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Jd")))) & (Bool (Set (Set (Var "Jc")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Jd"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "Jc"))) & (Bool (Set ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "Jd"))) & (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "Jc")))) & (Bool (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "Jc"))))) "holds" (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_1 :::"Component_of"::: ) (Set "(" ($#k2_connsp_3 :::"Down"::: ) "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set "(" (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "Jc")) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 3) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Jd")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "Jc")) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ")" ))))) ; registrationlet "C" be ($#m1_subset_1 :::"Simple_closed_curve":::); cluster (Set ($#k1_jordan2c :::"BDD"::: ) "C") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: JORDAN:97 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) "st" (Bool (Bool (Set (Var "U")) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Var "U")) "is" ($#v3_connsp_1 :::"a_component"::: ) )) "holds" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "P"))))))) ; theorem :: JORDAN:98 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "ex" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A2")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A2")))) & (Bool "(" "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) "st" (Bool (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "A1"))) & (Bool (Set (Var "C2")) ($#r1_hidden :::"="::: ) (Set (Var "A2")))) "holds" (Bool "(" (Bool (Set (Var "C1")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) ")" ) ")" ) ")" ))) ; theorem :: JORDAN:99 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set (Var "C")) "is" ($#v1_jordan1 :::"Jordan"::: ) )) ;