:: JORDAN5A  semantic presentation begin  
theorem :: JORDAN5A:1 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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 "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "P")) "is"   ($#v2_compts_1 :::"compact"::: )  )))) ; 
 
theorem :: JORDAN5A:2 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set  "(" (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "r1")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "r1"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "r2")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "r2"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" ))) "or" (Bool (Set (Var "r1"))  ($#r1_hidden :::"="::: )  (Set (Var "r2"))) "or" (Bool (Set (Var "p1"))  ($#r1_hidden :::"="::: )  (Set (Var "p2")))  ")" )))) ; 
 
theorem :: JORDAN5A:3 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2")))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) ")"  ")" ) ")" ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "x")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" )))  ")" ) & (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (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")))  ")" )))) ; 
 registrationlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k15_euclid :::"TOP-REAL"::: )  "n") ->   ($#v1_borsuk_2 :::"pathwise_connected"::: )   ; 
end; registrationlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v6_pre_topc :::"T_0"::: )     ($#v7_pre_topc :::"T_1"::: )     ($#v8_pre_topc :::"T_2"::: )     ($#v1_compts_1 :::"compact"::: )    for    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  "n"); 
end; 
theorem :: JORDAN5A:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "b"))  (Bool  "for" (Set (Var "P")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_compts_1 :::"compact"::: )     ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Num 2))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "P"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g"))  ($#r1_funct_2 :::"="::: )  (Set (Var "f"))) & (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Var "g")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))))) ; 
 begin  
theorem :: JORDAN5A:5 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_pcomps_1 :::"Family_open_set"::: )  (Set  ($#k8_metric_1 :::"RealSpace"::: ) ))) "iff" (Bool (Set (Var "X")) "is"   ($#v3_rcomp_1 :::"open"::: )  )  ")" )) ; 
 
theorem :: JORDAN5A:6 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_tmap_1 :::"is_continuous_at"::: )  (Set (Var "x"))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x1")))) "holds"  (Bool (Set (Var "g"))  ($#r1_fcont_1 :::"is_continuous_in"::: )  (Set (Var "x1"))))))) ; 
 
theorem :: JORDAN5A:7 (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Var "g")) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: JORDAN5A:8 (Bool  "for" (Set (Var "f")) "being"   ($#v2_funct_1 :::"one-to-one"::: )     ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "holds"  (Bool  "("  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "fx")) "," (Set (Var "fy")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) & (Bool (Set (Var "fx"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Var "fy"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Var "fx"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "fy"))))) "or" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "fx")) "," (Set (Var "fy")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) & (Bool (Set (Var "fx"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Var "fy"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Var "fx"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "fy")))))  ")" )) ; 
 
theorem :: JORDAN5A:9 (Bool  "for" (Set (Var "r")) "," (Set (Var "gg")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "r"))) & (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "r"))  ($#k9_real_1 :::"-"::: )  (Set (Var "gg")) ")" ) "," (Set  "(" (Set (Var "r"))  ($#k7_real_1 :::"+"::: )  (Set (Var "gg")) ")" ) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "r"))  ($#k9_real_1 :::"-"::: )  (Set (Var "gg")) ")" ) "," (Set  "(" (Set (Var "r"))  ($#k7_real_1 :::"+"::: )  (Set (Var "gg")) ")" ) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "x")) "," (Set (Var "gg")) ")" )))) ; 
 
theorem :: JORDAN5A:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Bool  "not" (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool (Bool  "not" (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_pcomps_1 :::"Family_open_set"::: )  (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )))) "holds"  (Bool (Set (Var "X")) "is"   ($#v3_rcomp_1 :::"open"::: )  ))) ; 
 
theorem :: JORDAN5A:11 (Bool  "for" (Set (Var "X")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool  "("  (Bool (Bool  "not" (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool (Bool  "not" (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))  ")" ))) ; 
 
theorem :: JORDAN5A:12 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  "st" (Bool (Bool (Set (Var "V"))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set (Var "X")) "is"   ($#v3_rcomp_1 :::"open"::: )  )) "holds"  (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_pcomps_1 :::"Family_open_set"::: )  (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )))))) ; 
 
theorem :: JORDAN5A:13 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")"  ")" )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d"))) & (Bool (Set (Var "f"))  ($#r1_tmap_1 :::"is_continuous_at"::: )  (Set (Var "x"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x1")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))  ($#r1_fcont_1 :::"is_continuous_in"::: )  (Set (Var "x1"))))))) ; 
 
theorem :: JORDAN5A:14 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")"  ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d"))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "d")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  )))) ; 
 begin  
theorem :: JORDAN5A:15 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")"  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d"))) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "d")))) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "fx")) "," (Set (Var "fy")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) & (Bool (Set (Var "fx"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Var "fy"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Var "fx"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "fy"))))))) ; 
 
theorem :: JORDAN5A:16 (Bool  "for" (Set (Var "f")) "being"   ($#v2_funct_1 :::"one-to-one"::: )     ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  ($#k5_topmetr :::"I[01]"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "fx")) "," (Set (Var "fy")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) & (Bool (Set (Var "fx"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Var "fy"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Var "fx"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "fy")))))) ; 
 
theorem :: JORDAN5A:17 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")"  ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  (Bool  "for" (Set (Var "PP")) "," (Set (Var "QQ")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d"))) & (Bool (Set (Var "PP"))  ($#r1_hidden :::"="::: )  (Set (Var "P"))) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "PP")) "is"   ($#v2_compts_1 :::"compact"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) & (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set (Var "QQ")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set  "("  ($#k1_weierstr :::"[#]"::: )  (Set (Var "PP")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "("  ($#k1_weierstr :::"[#]"::: )  (Set (Var "QQ")) ")" ))))))) ; 
 
theorem :: JORDAN5A:18 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")"  ")" )  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  (Bool  "for" (Set (Var "PP")) "," (Set (Var "QQ")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d"))) & (Bool (Set (Var "PP"))  ($#r1_hidden :::"="::: )  (Set (Var "P"))) & (Bool (Set (Var "QQ"))  ($#r1_hidden :::"="::: )  (Set (Var "Q"))) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "PP")) "is"   ($#v2_compts_1 :::"compact"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) & (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set (Var "Q")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set  "("  ($#k1_weierstr :::"[#]"::: )  (Set (Var "PP")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "("  ($#k1_weierstr :::"[#]"::: )  (Set (Var "QQ")) ")" ))))))) ; 
 
theorem :: JORDAN5A:19 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool  "("  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )) ; 
 
theorem :: JORDAN5A:20 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")"  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d"))) & (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "f"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "e"))) & (Bool (Set (Var "f"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "F")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))) & (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "F"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "e")) "," (Set (Var "f")) ($#k1_rcomp_1 :::".]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "g")) "," (Set (Var "h")) ($#k1_rcomp_1 :::".]"::: ) )))) ; 
 
theorem :: JORDAN5A:21 (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Q"))) & (Bool (Set (Set (Var "P"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Q"))) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2")))) "holds"  (Bool  "ex" (Set (Var "EX")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "EX"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "P"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Q")))) & (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "P")) ")" )(Bool  "ex" (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "g")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p1"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p2"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s2")))  ($#r1_hidden :::"="::: )  (Set (Var "EX"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s2"))) & (Bool (Set (Var "s2"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "t"))) & (Bool (Set (Var "t"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s2")))) "holds"  (Bool  "not" (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "t")))  ($#r2_hidden :::"in"::: )  (Set (Var "Q"))))  ")" )  ")" )))  ")" )))) ; 
 
theorem :: JORDAN5A:22 (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Q"))) & (Bool (Set (Set (Var "P"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Q"))) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2")))) "holds"  (Bool  "ex" (Set (Var "EX")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "EX"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "P"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Q")))) & (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "P")) ")" )(Bool  "ex" (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "g")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p1"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p2"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s2")))  ($#r1_hidden :::"="::: )  (Set (Var "EX"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s2"))) & (Bool (Set (Var "s2"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::">="::: )  (Set (Var "t"))) & (Bool (Set (Var "t"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "s2")))) "holds"  (Bool  "not" (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "t")))  ($#r2_hidden :::"in"::: )  (Set (Var "Q"))))  ")" )  ")" )))  ")" )))) ; 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  bbbadV1_MEMBERED() bbbadV2_MEMBERED() bbbadV3_MEMBERED()   ($#v1_finset_1 :::"finite"::: )     ($#v5_xxreal_2 :::"real-bounded"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 
end; 
theorem :: JORDAN5A:23 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) "holds"  (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v2_rcomp_1 :::"closed"::: )  ) "iff" (Bool (Set (Var "B")) "is"   ($#v4_pre_topc :::"closed"::: )  )  ")" ))) ; 
 
theorem :: JORDAN5A:24 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k6_measure6 :::"Cl"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "B")))))) ; 
 registrationlet "a", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set bbbadK1_XXREAL_1("a" "," "b")) ->   ($#v1_rcomp_1 :::"compact"::: )    for  ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); 
end; 
theorem :: JORDAN5A:25 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) "holds"  (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v1_rcomp_1 :::"compact"::: )  ) "iff" (Bool (Set (Var "B")) "is"   ($#v2_compts_1 :::"compact"::: )  )  ")" ))) ; 
 registration
cluster   ($#v1_finset_1 :::"finite"::: )    ->   ($#v1_rcomp_1 :::"compact"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 
end; 
theorem :: JORDAN5A:26 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) "iff" (Bool (Set   ($#k6_measure6 :::"Cl"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))  ")" )) ; 
 
theorem :: JORDAN5A:27 (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set (Var "g")))) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_pscomp_1 :::"continuous"::: )  ) "iff" (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ;