:: JORDAN10  semantic presentation begin  registration
cluster bbbadV4_FUNCT_1()   ($#v2_connsp_1 :::"connected"::: )     ($#v2_compts_1 :::"compact"::: )    ($#~v1_sppol_1  "non"   ($#v1_sppol_1 :::"horizontal"::: )   )   ($#~v2_sppol_1  "non"   ($#v2_sppol_1 :::"vertical"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))); 
end; 












theorem :: JORDAN10:1 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))) "holds"  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN10:2 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )) & (Bool (Set (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds"  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)))) ; 
 
theorem :: JORDAN10:3 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")" ))) "holds"  (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)))) ; 
 
theorem :: JORDAN10:4 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")" )) & (Bool (Set (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds"  (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN10:5 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Var "C"))  ($#r1_subset_1 :::"misses"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN10:6 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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   ($#k7_pscomp_1 :::"N-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_pscomp_1 :::"N-bound"::: )  (Set (Var "C")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k7_pscomp_1 :::"N-bound"::: )  (Set (Var "C")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k9_pscomp_1 :::"S-bound"::: )  (Set (Var "C")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k13_newton :::"|^"::: )  (Set (Var "n")) ")" ) ")" ))))) ; 
 
theorem :: JORDAN10:7 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j")))) "holds"  (Bool (Set   ($#k7_pscomp_1 :::"N-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "j")) ")"  ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k7_pscomp_1 :::"N-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "i")) ")"  ")" ) ")" ))))) ; 
 registrationlet "C" be   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" ); let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k3_goboard9 :::"RightComp"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" "C" "," "n" ")"  ")" ) ")" )) ->   ($#v2_compts_1 :::"compact"::: )   ; 
end; 
theorem :: JORDAN10:8 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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   ($#k20_pscomp_1 :::"N-min"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_goboard9 :::"RightComp"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN10:9 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Var "C"))  ($#r2_subset_1 :::"meets"::: )  (Set   ($#k3_goboard9 :::"RightComp"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN10:10 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Var "C"))  ($#r1_subset_1 :::"misses"::: )  (Set   ($#k2_goboard9 :::"LeftComp"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN10:11 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Var "C"))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_goboard9 :::"RightComp"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN10:12 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Var "C"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ))))) ; 
 
theorem :: JORDAN10:13 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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_jordan2c :::"UBD"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_jordan2c :::"UBD"::: )  (Set (Var "C")))))) ; 
 definitionlet "C" be   ($#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) ")" ); func  :::"UBD-Family"::: "C" ->    ($#m1_hidden :::"set"::: )   equals :: JORDAN10:def 1  "{"  (Set  "("  ($#k2_jordan2c :::"UBD"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" "C" "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) where n "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool verum)  "}"  ; func  :::"BDD-Family"::: "C" ->    ($#m1_hidden :::"set"::: )   equals :: JORDAN10:def 2  "{"  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_jordan2c :::"BDD"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" "C" "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" ) where n "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool verum)  "}"  ; end; 










:: deftheorem    defines :::"UBD-Family"::: JORDAN10:def 1 :  (Bool  "for" (Set (Var "C")) "being"   ($#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   ($#k1_jordan10 :::"UBD-Family"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k2_jordan2c :::"UBD"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) where n "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool verum)  "}"  )); 
 
:: deftheorem    defines :::"BDD-Family"::: JORDAN10:def 2 :  (Bool  "for" (Set (Var "C")) "being"   ($#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_jordan10 :::"BDD-Family"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_jordan2c :::"BDD"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" ) where n "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool verum)  "}"  )); 
 definitionlet "C" be   ($#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) ")" ); :: original: :::"UBD-Family"::: redefine func  :::"UBD-Family"::: "C" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); :: original: :::"BDD-Family"::: redefine func  :::"BDD-Family"::: "C" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); end; registrationlet "C" be   ($#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) ")" ); 
cluster (Set   ($#k1_jordan10 :::"UBD-Family"::: )  "C") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set   ($#k2_jordan10 :::"BDD-Family"::: )  "C") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: JORDAN10:14 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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   ($#k5_setfam_1 :::"union"::: )  (Set  "("  ($#k3_jordan10 :::"UBD-Family"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_jordan2c :::"UBD"::: )  (Set (Var "C"))))) ; 
 
theorem :: JORDAN10:15 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Var "C"))  ($#r1_tarski :::"c="::: )  (Set   ($#k6_setfam_1 :::"meet"::: )  (Set  "("  ($#k4_jordan10 :::"BDD-Family"::: )  (Set (Var "C")) ")" )))) ; 
 
theorem :: JORDAN10:16 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k2_goboard9 :::"LeftComp"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN10:17 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_goboard9 :::"RightComp"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN10:18 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_jordan2c :::"is_inside_component_of"::: )  (Set (Var "C")))) "holds"  (Bool (Set (Var "P"))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: JORDAN10:19 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN10:20 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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   ($#k7_setfam_1 :::"COMPLEMENT"::: )  (Set  "("  ($#k3_jordan10 :::"UBD-Family"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_jordan10 :::"BDD-Family"::: )  (Set (Var "C"))))) ; 
 
theorem :: JORDAN10:21 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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   ($#k6_setfam_1 :::"meet"::: )  (Set  "("  ($#k4_jordan10 :::"BDD-Family"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C")) ")" )))) ;