:: JORDAN11  semantic presentation begin  








definitionlet "C" be   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); func  :::"ApproxIndex"::: "C" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: JORDAN11:def 1 (Bool  "("  (Bool it  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  "C") & (Bool  "("   "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  "C")) "holds"  (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">="::: )  it)  ")" )  ")" ); end; 





:: deftheorem    defines :::"ApproxIndex"::: JORDAN11:def 1 :  (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "b2")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")))) "iff" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Var "C"))) & (Bool  "("   "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Var "C")))) "holds"  (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "b2")))  ")" )  ")" )  ")" ))); 
 
theorem :: JORDAN11:1 (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) ; 
 definitionlet "C" be   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); func  :::"Y-InitStart"::: "C" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: JORDAN11:def 2 (Bool  "("  (Bool it  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  "C" ")" ) ")"  ")" ))) & (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  "C" ")" ) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" "C" "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  "C" ")" ) ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," it ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  "C")) & (Bool  "("   "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  "C" ")" ) ")"  ")" ))) & (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  "C" ")" ) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" "C" "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  "C" ")" ) ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  "C"))) "holds"  (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">="::: )  it)  ")" )  ")" ); end; 





:: deftheorem    defines :::"Y-InitStart"::: JORDAN11:def 2 :  (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "b2")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_jordan11 :::"Y-InitStart"::: )  (Set (Var "C")))) "iff" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")) ")" ) ")"  ")" ))) & (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")) ")" ) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")) ")" ) ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "b2")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C")))) & (Bool  "("   "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")) ")" ) ")"  ")" ))) & (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")) ")" ) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")) ")" ) ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "b2")))  ")" )  ")" )  ")" ))); 
 
theorem :: JORDAN11:2 (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "holds" (Bool (Set   ($#k2_jordan11 :::"Y-InitStart"::: )  (Set (Var "C")))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) ; 
 
theorem :: JORDAN11:3 (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "holds" (Bool (Set (Set  "("  ($#k2_jordan11 :::"Y-InitStart"::: )  (Set (Var "C")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")) ")" ) ")"  ")" )))) ; 
 definitionlet "C" be   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); let "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); assume 
(Bool (Set (Const "n"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Const "C")))
 ; func  :::"Y-SpanStart":::  "(" "C" "," "n" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: JORDAN11:def 3 (Bool  "("  (Bool it  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")"  ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool it  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k13_newton :::"|^"::: )  (Set  "(" "n"  ($#k7_nat_d :::"-'"::: )  (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  "C" ")" ) ")" ) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k2_jordan11 :::"Y-InitStart"::: )  "C" ")" )  ($#k7_nat_d :::"-'"::: )  (Num 2) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 2)))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")"  ")" ) "," (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" "C" "," "n" ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  "C"))  ")" ) & (Bool  "("   "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")"  ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k13_newton :::"|^"::: )  (Set  "(" "n"  ($#k7_nat_d :::"-'"::: )  (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  "C" ")" ) ")" ) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k2_jordan11 :::"Y-InitStart"::: )  "C" ")" )  ($#k7_nat_d :::"-'"::: )  (Num 2) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 2)))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")"  ")" ) "," (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" "C" "," "n" ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  "C"))  ")" )) "holds"  (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">="::: )  it)  ")" )  ")" ); end; 







:: deftheorem    defines :::"Y-SpanStart"::: JORDAN11:def 3 :  (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Var "C")))) "holds"  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "b3"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")) ")" ) ")" ) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k2_jordan11 :::"Y-InitStart"::: )  (Set (Var "C")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 2) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 2)))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C"))))  ")" ) & (Bool  "("   "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")) ")" ) ")" ) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k2_jordan11 :::"Y-InitStart"::: )  (Set (Var "C")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 2) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 2)))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C"))))  ")" )) "holds"  (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "b3")))  ")" )  ")" )  ")" )))); 
 
theorem :: JORDAN11:4 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Var "C")))) "holds"  (Bool (Set   ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")) ")" ) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")) ")" ) ")"  ")" )  ($#k9_real_1 :::"-"::: )  (Num 2) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Num 2))))) ; 
 
theorem :: JORDAN11:5 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Var "C")))) "holds"  (Bool (Set   ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set  "("  ($#k1_jordan11 :::"ApproxIndex"::: )  (Set (Var "C")) ")" ) ")" ) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k2_jordan11 :::"Y-InitStart"::: )  (Set (Var "C")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 2) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 2))))) ; 
 
theorem :: JORDAN11:6 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Var "C")))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set  "("  ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C")))))) ; 
 
theorem :: JORDAN11:7 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Var "C")))) "holds"  (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set   ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )))  ")" ))) ; 
 
theorem :: JORDAN11:8 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Var "C")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) "," (Set  "("  ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN11:9 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Var "C")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set  "("  ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN11:10 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Var "C")))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set  "(" (Set  "("  ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "C"))))) ; 
 
theorem :: JORDAN11:11 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Var "C")))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set  "("  ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "C"))))) ; 
 begin  







theorem :: JORDAN11:12 (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  "holds" (Bool (Set   ($#k2_jordan2c :::"UBD"::: )  (Set (Var "C")))  ($#r2_subset_1 :::"meets"::: )  (Set   ($#k2_jordan2c :::"UBD"::: )  (Set (Var "D")))))) ; 
 
theorem :: JORDAN11:13 (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "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 (Var "C")))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C"))))) "holds"  (Bool (Set   ($#k5_jordan1k :::"dist"::: )   "(" (Set (Var "q")) "," (Set (Var "C")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_topreal6 :::"dist"::: )   "(" (Set (Var "q")) "," (Set (Var "p")) ")" )))) ; 
 
theorem :: JORDAN11:14 (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#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 (Bool  "not" (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C")))))) "holds"  (Bool (Set   ($#k5_jordan1k :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_jordan1k :::"dist"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C")) ")" ) ")" )))) ; 
 
theorem :: JORDAN11:15 (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "D")))) "or"  "not" (Bool (Set (Var "D"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C"))))  ")" ))) ; 
 
theorem :: JORDAN11:16 (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "D"))))) "holds"  (Bool (Set (Var "D"))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_jordan2c :::"UBD"::: )  (Set (Var "C")))))) ; 
 
theorem :: JORDAN11:17 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_jordan2c :::"UBD"::: )  (Set (Var "C")))))) ;