:: JORDAN2C semantic presentation begin registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k15_euclid :::"TOP-REAL"::: ) "n") -> ($#v6_rltopsp1 :::"add-continuous"::: ) ($#v7_rltopsp1 :::"Mult-continuous"::: ) ; end; begin theorem :: JORDAN2C:1 canceled; theorem :: JORDAN2C:2 canceled; theorem :: JORDAN2C:3 canceled; theorem :: JORDAN2C:4 canceled; theorem :: JORDAN2C:5 canceled; theorem :: JORDAN2C:6 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#v5_valued_0 :::"increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" ))) ; theorem :: JORDAN2C:7 canceled; theorem :: JORDAN2C:8 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )))) ; theorem :: JORDAN2C:9 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "q1")) ($#k12_euclid :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "q2")) ($#k12_euclid :::".|"::: ) ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "q1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q2")) ")" ) ($#k12_euclid :::".|"::: ) )))) ; theorem :: JORDAN2C:10 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set ($#k1_jordan2b :::"|["::: ) (Set (Var "r")) ($#k1_jordan2b :::"]|"::: ) ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "r"))))) ; theorem :: JORDAN2C:11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v9_rltopsp1 :::"bounded"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v6_tbsp_1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" )) ")" ))) ; theorem :: JORDAN2C:12 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B")) "is" ($#v9_rltopsp1 :::"bounded"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; definitioncanceled; let "n" be ($#m1_hidden :::"Nat":::); let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); pred "B" :::"is_inside_component_of"::: "A" means :: JORDAN2C:def 2 (Bool "(" (Bool "B" ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set "A" ($#k3_subset_1 :::"`"::: ) )) & (Bool "B" "is" ($#v9_rltopsp1 :::"bounded"::: ) ) ")" ); end; :: deftheorem JORDAN2C:def 1 : canceled; :: deftheorem defines :::"is_inside_component_of"::: JORDAN2C:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "B")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )) & (Bool (Set (Var "B")) "is" ($#v9_rltopsp1 :::"bounded"::: ) ) ")" ) ")" ))); registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; cluster ($#v6_tbsp_1 :::"bounded"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")); end; theorem :: JORDAN2C:13 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "A"))) "iff" (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "C")) "is" ($#v6_tbsp_1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" )) ")" )) ")" ))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); pred "B" :::"is_outside_component_of"::: "A" means :: JORDAN2C:def 3 (Bool "(" (Bool "B" ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set "A" ($#k3_subset_1 :::"`"::: ) )) & (Bool (Bool "not" "B" "is" ($#v9_rltopsp1 :::"bounded"::: ) )) ")" ); end; :: deftheorem defines :::"is_outside_component_of"::: JORDAN2C:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "B")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )) & (Bool (Bool "not" (Set (Var "B")) "is" ($#v9_rltopsp1 :::"bounded"::: ) )) ")" ) ")" ))); theorem :: JORDAN2C:14 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "A"))) "iff" (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "C")) "is" (Bool "not" ($#v6_tbsp_1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ))) ")" )) ")" ))) ; theorem :: JORDAN2C:15 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: JORDAN2C:16 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); func :::"BDD"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) equals :: JORDAN2C:def 4 (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) : (Bool (Set (Var "B")) ($#r1_jordan2c :::"is_inside_component_of"::: ) "A") "}" ); end; :: deftheorem defines :::"BDD"::: JORDAN2C:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set (Var "B")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "A"))) "}" )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); func :::"UBD"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) equals :: JORDAN2C:def 5 (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) : (Bool (Set (Var "B")) ($#r2_jordan2c :::"is_outside_component_of"::: ) "A") "}" ); end; :: deftheorem defines :::"UBD"::: JORDAN2C:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set (Var "B")) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "A"))) "}" )))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" )) -> ($#v1_convex1 :::"convex"::: ) ; end; registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" )) -> ($#v3_connsp_1 :::"a_component"::: ) ; end; theorem :: JORDAN2C:17 canceled; theorem :: JORDAN2C:18 canceled; theorem :: JORDAN2C:19 canceled; theorem :: JORDAN2C:20 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set (Var "A"))) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ))))) ; theorem :: JORDAN2C:21 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "A"))) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ))))) ; theorem :: JORDAN2C:22 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k1_jordan2c :::"BDD"::: ) (Set (Var "A")))))) ; theorem :: JORDAN2C:23 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "A")))))) ; theorem :: JORDAN2C:24 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set (Var "A"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "A")))))) ; theorem :: JORDAN2C:25 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: JORDAN2C:26 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: JORDAN2C:27 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set "(" ($#k1_jordan2c :::"BDD"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_jordan2c :::"UBD"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: JORDAN2C:28 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "P")) "is" ($#v2_connsp_1 :::"connected"::: ) ))) ; theorem :: JORDAN2C:29 canceled; theorem :: JORDAN2C:30 canceled; theorem :: JORDAN2C:31 canceled; theorem :: JORDAN2C:32 canceled; theorem :: JORDAN2C:33 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))))) "holds" (Bool "not" (Bool (Set (Var "W")) "is" ($#v6_tbsp_1 :::"bounded"::: ) )))) ; theorem :: JORDAN2C:34 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v9_rltopsp1 :::"bounded"::: ) ) "iff" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))))) ")" ))) ; theorem :: JORDAN2C:35 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "not" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; theorem :: JORDAN2C:36 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k2_jordan2c :::"UBD"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))))) ; theorem :: JORDAN2C:37 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "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 (Var "h1")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h1")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "w2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h1")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "h2")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "w2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h2")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "w3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h2")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "h3")) "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 (Var "h3")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h3")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "w3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h3")) ($#k1_funct_1 :::"."::: ) (Num 1))) ")" )))))) ; theorem :: JORDAN2C:38 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "w3")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w2")) "," (Set (Var "w3")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "ex" (Set (Var "h")) "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 (Var "h")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "w3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Num 1))) ")" ))))) ; theorem :: JORDAN2C:39 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) "," (Set (Var "w4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "w3")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "w4")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w2")) "," (Set (Var "w3")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w3")) "," (Set (Var "w4")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "ex" (Set (Var "h")) "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 (Var "h")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "w4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Num 1))) ")" ))))) ; theorem :: JORDAN2C:40 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) "," (Set (Var "w4")) "," (Set (Var "w5")) "," (Set (Var "w6")) "," (Set (Var "w7")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "w3")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "w4")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "w5")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "w6")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "w7")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w2")) "," (Set (Var "w3")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w3")) "," (Set (Var "w4")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w4")) "," (Set (Var "w5")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w5")) "," (Set (Var "w6")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w6")) "," (Set (Var "w7")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "ex" (Set (Var "h")) "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 (Var "h")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "w7")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Num 1))) ")" ))))) ; theorem :: JORDAN2C:41 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "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 "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" )) & (Bool (Bool "not" (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" )))) "holds" (Bool "ex" (Set (Var "w0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "w0")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" )) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "w0")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "w0")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ))) ")" ))))) ; theorem :: JORDAN2C:42 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a"))) "}" ) & (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w4")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w4"))))) & (Bool (Bool "not" (Set (Var "w4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w1"))))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "w2")) "," (Set (Var "w3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w3")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w2")) "," (Set (Var "w3")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w3")) "," (Set (Var "w4")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) ")" )))))) ; theorem :: JORDAN2C:43 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) ($#k6_subset_1 :::"\"::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) "}" )) & (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w4")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w4"))))) & (Bool (Bool "not" (Set (Var "w4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w1"))))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "w2")) "," (Set (Var "w3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w3")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w2")) "," (Set (Var "w3")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w3")) "," (Set (Var "w4")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) ")" )))))) ; theorem :: JORDAN2C:44 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" )) ")" )) ; theorem :: JORDAN2C:45 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "x"))))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ))))) ; theorem :: JORDAN2C:46 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: JORDAN2C:47 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "x"))))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "y"))))) ")" ))))) ; theorem :: JORDAN2C:48 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w7")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a"))) "}" ) & (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w7")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w7")))) "or" (Bool (Set (Var "w7")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w1")))) ")" ))) "holds" (Bool "ex" (Set (Var "w2")) "," (Set (Var "w3")) "," (Set (Var "w4")) "," (Set (Var "w5")) "," (Set (Var "w6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w3")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w4")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w5")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w6")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w2")) "," (Set (Var "w3")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w3")) "," (Set (Var "w4")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w4")) "," (Set (Var "w5")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w5")) "," (Set (Var "w6")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w6")) "," (Set (Var "w7")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) ")" )))))) ; theorem :: JORDAN2C:49 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w7")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) ($#k6_subset_1 :::"\"::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) "}" )) & (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w7")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w7")))) "or" (Bool (Set (Var "w7")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w1")))) ")" ))) "holds" (Bool "ex" (Set (Var "w2")) "," (Set (Var "w3")) "," (Set (Var "w4")) "," (Set (Var "w5")) "," (Set (Var "w6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w3")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w4")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w5")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "w6")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w2")) "," (Set (Var "w3")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w3")) "," (Set (Var "w4")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w4")) "," (Set (Var "w5")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w5")) "," (Set (Var "w6")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w6")) "," (Set (Var "w7")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) ")" )))))) ; theorem :: JORDAN2C:50 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a"))) "}" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: JORDAN2C:51 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v2_connsp_1 :::"connected"::: ) )))) ; theorem :: JORDAN2C:52 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) ($#k6_subset_1 :::"\"::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) "}" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: JORDAN2C:53 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) ($#k6_subset_1 :::"\"::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) "}" ))) "holds" (Bool (Set (Var "P")) "is" ($#v2_connsp_1 :::"connected"::: ) )))) ; theorem :: JORDAN2C:54 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) ($#k6_subset_1 :::"\"::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) "}" ))) "holds" (Bool "not" (Bool (Set (Var "P")) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))))) ; theorem :: JORDAN2C:55 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 1) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 1) ")" ) : (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a"))) ")" )) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v1_convex1 :::"convex"::: ) ))) ; theorem :: JORDAN2C:56 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 1) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 1) ")" ) : (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_real_1 :::"-"::: ) (Set (Var "a")))) ")" )) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v1_convex1 :::"convex"::: ) ))) ; theorem :: JORDAN2C:57 canceled; theorem :: JORDAN2C:58 canceled; theorem :: JORDAN2C:59 (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 1) ")" ) : (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a"))) ")" )) "}" )) "holds" (Bool "not" (Bool (Set (Var "W")) "is" ($#v6_tbsp_1 :::"bounded"::: ) )))) ; theorem :: JORDAN2C:60 (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 1) ")" ) : (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_real_1 :::"-"::: ) (Set (Var "a")))) ")" )) "}" )) "holds" (Bool "not" (Bool (Set (Var "W")) "is" ($#v6_tbsp_1 :::"bounded"::: ) )))) ; theorem :: JORDAN2C:61 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a"))) "}" )) "holds" (Bool "not" (Bool (Set (Var "W")) "is" ($#v6_tbsp_1 :::"bounded"::: ) ))))) ; theorem :: JORDAN2C:62 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) ($#k6_subset_1 :::"\"::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) "}" ))) "holds" (Bool "not" (Bool (Set (Var "W")) "is" ($#v6_tbsp_1 :::"bounded"::: ) ))))) ; theorem :: JORDAN2C:63 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "P1")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Set (Var "P")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Bool "not" (Set (Var "W")) "is" ($#v6_tbsp_1 :::"bounded"::: ) )) & (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set "(" ($#k4_connsp_3 :::"Down"::: ) "(" (Set (Var "P")) "," (Set "(" (Set (Var "Q")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ")" ))) & (Bool (Set (Var "W")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Var "P1")) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "Q")))))) ; theorem :: JORDAN2C:64 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) ($#k1_topmetr :::"|"::: ) (Set (Var "B")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) "is" ($#v6_tbsp_1 :::"bounded"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v6_tbsp_1 :::"bounded"::: ) ))))) ; theorem :: JORDAN2C:65 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#v2_compts_1 :::"compact"::: ) -> ($#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" ")" ))); end; theorem :: JORDAN2C:66 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "A")) "is" ($#v9_rltopsp1 :::"bounded"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: JORDAN2C:67 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" )) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q1")) where q1 "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q1")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" )) "holds" (Bool (Set (Var "A")) "is" ($#v6_tbsp_1 :::"bounded"::: ) ) ")" ) ")" ))) ; theorem :: JORDAN2C:68 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool (Set (Var "A")) "is" ($#v9_rltopsp1 :::"bounded"::: ) )) "holds" (Bool (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "A"))) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "A"))))) ; theorem :: JORDAN2C:69 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v1_convex1 :::"convex"::: ) )))) ; theorem :: JORDAN2C:70 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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_hidden :::"="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "a")) ")" ))) "holds" (Bool (Set (Var "P")) "is" ($#v1_convex1 :::"convex"::: ) ))))) ; theorem :: JORDAN2C:71 canceled; theorem :: JORDAN2C:72 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "h")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) ")" )))))) ; theorem :: JORDAN2C:73 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "h")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ")" ))) ")" ))))))) ; theorem :: JORDAN2C:74 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "ex" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "f1")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f1"))) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" )))))))) ; theorem :: JORDAN2C:75 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#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")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "R")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" "not" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "or" "not" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) "or" "not" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) "or" "not" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ) ")" ) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))))) ; theorem :: JORDAN2C:76 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "R")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "R")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) "or" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" )) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) )))) ; theorem :: JORDAN2C:77 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) "or" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" )) ")" ) "}" )) "holds" (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R")))))) ; theorem :: JORDAN2C:78 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#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 (Set (Var "R")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "R")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) "or" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" )) ")" ) "}" )) "holds" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))))) ; theorem :: JORDAN2C:79 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "R")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))))) ; theorem :: JORDAN2C:80 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) "}" )) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )))) ; theorem :: JORDAN2C:81 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "B"))) "is" ($#v1_connsp_2 :::"locally_connected"::: ) ))) ; theorem :: JORDAN2C:82 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) "}" ) & (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "B"))) "is" ($#v1_connsp_2 :::"locally_connected"::: ) ))))) ; theorem :: JORDAN2C:83 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; theorem :: JORDAN2C:84 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )) ")" ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ))) ; theorem :: JORDAN2C:85 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" ) ($#k12_euclid :::".|"::: ) )) ")" ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )))) ; theorem :: JORDAN2C:86 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "g")) ($#k10_funct_2 :::"/."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "g")) ($#k10_funct_2 :::"/."::: ) (Num 1) ")" ) ($#k12_euclid :::".|"::: ) ))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "g")) ($#k10_funct_2 :::"/."::: ) (Set (Var "s")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a"))))))) ; theorem :: JORDAN2C:87 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "r"))))))) ; theorem :: JORDAN2C:88 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) "}" )) "holds" (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set (Var "A"))) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "A")))))) ; begin theorem :: JORDAN2C:89 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k2_goboard2 :::"GoB"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k2_goboard2 :::"GoB"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_goboard2 :::"GoB"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 2) ")" )) & (Bool (Set (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_goboard2 :::"GoB"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 2) "," (Num 2) ")" )) & (Bool (Set (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_goboard2 :::"GoB"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 2) "," (Num 1) ")" )) & (Bool (Set (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_goboard2 :::"GoB"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" )) & (Bool (Set (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 5)) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_goboard2 :::"GoB"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 2) ")" )) ")" )) ; theorem :: JORDAN2C:90 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Bool "not" (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" )) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; theorem :: JORDAN2C:91 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" )))) ; theorem :: JORDAN2C:92 (Bool "for" (Set (Var "G")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "C")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: JORDAN2C:93 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) )) & (Bool (Bool "not" (Set (Var "B")) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ))))) ; theorem :: JORDAN2C:94 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set ($#k3_goboard9 :::"RightComp"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_jordan2c :::"BDD"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" ))) & (Bool (Set ($#k3_goboard9 :::"RightComp"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" )) "is" ($#v9_rltopsp1 :::"bounded"::: ) ) ")" )) ; theorem :: JORDAN2C:95 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" ))) & (Bool (Set ($#k3_goboard9 :::"RightComp"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan2c :::"BDD"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" ))) ")" )) ; theorem :: JORDAN2C:96 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set ($#k2_jordan2c :::"UBD"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_jordan2c :::"UBD"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" )) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ))) & (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" )) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ))) ")" )) ; begin theorem :: JORDAN2C:97 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )) & (Bool (Set (Var "V")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "B"))) ")" )))) ")" ))) ; theorem :: JORDAN2C:98 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ) & (Bool (Set (Var "A")) "is" ($#v1_jordan1 :::"Jordan"::: ) ) ")" ) "iff" (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 "A")) ($#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 (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A1")))) & (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 "A")) ($#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 :: JORDAN2C:99 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "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 "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (Bool (Set (Var "P")) "is" ($#v2_tops_1 :::"boundary"::: ) )))) ; theorem :: JORDAN2C:100 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q"))))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))) ")" ))) ; theorem :: JORDAN2C:101 (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ) "is" ($#v2_tops_1 :::"boundary"::: ) )) ; registrationlet "q1", "q2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" "q1" "," "q2" ")" ) -> ($#v2_tops_1 :::"boundary"::: ) ; end; theorem :: JORDAN2C:102 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) "is" ($#v2_tops_1 :::"boundary"::: ) )) ; registrationlet "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k3_topreal1 :::"L~"::: ) "f") -> ($#v2_tops_1 :::"boundary"::: ) ; end; theorem :: JORDAN2C:103 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "ep")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "ep"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "ep")) "," (Set (Var "r")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "q")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ))))) ; theorem :: JORDAN2C:104 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" )))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" ))) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) ")" ))))) ; theorem :: JORDAN2C:105 (Bool (Set ($#k1_euclid :::"REAL"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k1_seq_4 :::"}"::: ) )) ; theorem :: JORDAN2C:106 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v9_rltopsp1 :::"bounded"::: ) )) "holds" (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set (Var "A"))) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; theorem :: JORDAN2C:107 (Bool "for" (Set (Var "G")) "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 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "C")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "C")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: JORDAN2C:108 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v9_rltopsp1 :::"bounded"::: ) ) & (Bool (Set (Var "A")) "is" ($#v1_jordan1 :::"Jordan"::: ) )) "holds" (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set (Var "A"))) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "A")))) ; theorem :: JORDAN2C:109 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" )))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k1_jordan2c :::"BDD"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" ) ")" ))) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) ")" ))))) ; begin theorem :: JORDAN2C:110 (Bool "for" (Set (Var "f")) "being" ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#v2_goboard5 :::"standard"::: ) ($#v1_sprect_2 :::"clockwise_oriented"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k20_pscomp_1 :::"N-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set (Var "f")))))) ; theorem :: JORDAN2C:111 (Bool "for" (Set (Var "f")) "being" ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#v2_goboard5 :::"standard"::: ) ($#v1_sprect_2 :::"clockwise_oriented"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k20_pscomp_1 :::"N-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set (Var "f")))))) ; theorem :: JORDAN2C:112 (Bool "for" (Set (Var "f")) "being" ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#v2_goboard5 :::"standard"::: ) ($#v1_sprect_2 :::"clockwise_oriented"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k20_pscomp_1 :::"N-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set (Var "f")))))) ; theorem :: JORDAN2C:113 (Bool "for" (Set (Var "f")) "being" ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#v2_goboard5 :::"standard"::: ) ($#v1_sprect_2 :::"clockwise_oriented"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k20_pscomp_1 :::"N-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set (Var "f")))))) ; theorem :: JORDAN2C:114 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) "is" ($#v2_connsp_1 :::"connected"::: ) ))) ; theorem :: JORDAN2C:115 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) "is" ($#v2_connsp_1 :::"connected"::: ) ))) ; theorem :: JORDAN2C:116 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) "is" ($#v2_connsp_1 :::"connected"::: ) ))) ; theorem :: JORDAN2C:117 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))))) ; theorem :: JORDAN2C:118 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "," (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "Q"))) & (Bool (Set (Var "R")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Var "P")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "R"))))) ; theorem :: JORDAN2C:119 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v9_rltopsp1 :::"bounded"::: ) ) & (Bool (Set (Var "A")) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "P"))) & (Bool (Set (Var "B")) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; registrationlet "C" be ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k1_jordan2c :::"BDD"::: ) "C") -> ($#v3_pre_topc :::"open"::: ) ; cluster (Set ($#k2_jordan2c :::"UBD"::: ) "C") -> ($#v3_pre_topc :::"open"::: ) ; end; registrationlet "C" be ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k2_jordan2c :::"UBD"::: ) "C") -> ($#v2_connsp_1 :::"connected"::: ) ; end; theorem :: JORDAN2C:120 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Bool "not" (Set ($#k7_topreal1 :::"west_halfline"::: ) (Set (Var "p"))) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; theorem :: JORDAN2C:121 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Bool "not" (Set ($#k5_topreal1 :::"east_halfline"::: ) (Set (Var "p"))) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; theorem :: JORDAN2C:122 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Bool "not" (Set ($#k4_topreal1 :::"north_halfline"::: ) (Set (Var "p"))) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; theorem :: JORDAN2C:123 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Bool "not" (Set ($#k6_topreal1 :::"south_halfline"::: ) (Set (Var "p"))) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; registrationlet "C" be ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k2_jordan2c :::"UBD"::: ) "C") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: JORDAN2C:124 (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 ($#k2_jordan2c :::"UBD"::: ) (Set (Var "C"))) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ))) ; theorem :: JORDAN2C:125 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "WH")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "WH")) "is" ($#v9_rltopsp1 :::"bounded"::: ) )) & (Bool (Set (Var "WH")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "WH")) ($#r1_tarski :::"c="::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "C")))))) ; theorem :: JORDAN2C:126 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k7_topreal1 :::"west_halfline"::: ) (Set (Var "p"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k7_topreal1 :::"west_halfline"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "C")))))) ; theorem :: JORDAN2C:127 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k5_topreal1 :::"east_halfline"::: ) (Set (Var "p"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k5_topreal1 :::"east_halfline"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "C")))))) ; theorem :: JORDAN2C:128 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k6_topreal1 :::"south_halfline"::: ) (Set (Var "p"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k6_topreal1 :::"south_halfline"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "C")))))) ; theorem :: JORDAN2C:129 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k4_topreal1 :::"north_halfline"::: ) (Set (Var "p"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k4_topreal1 :::"north_halfline"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "C")))))) ; theorem :: JORDAN2C:130 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "z")))) "holds" (Bool (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" )))))) ; theorem :: JORDAN2C:131 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "s")) ")" ) ")" )))))) ; theorem :: JORDAN2C:132 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) "holds" (Bool "for" (Set (Var "BA")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "BA")) ($#r1_hidden :::"="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set (Var "s")) ($#k1_convex1 :::"*"::: ) (Set (Var "BA"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "t")) ($#k1_convex1 :::"*"::: ) (Set (Var "BA")))))))) ;