:: JORDAN5B  semantic presentation begin  
theorem :: JORDAN5B:1 (Bool  "for" (Set (Var "i1")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1")))) "holds"  (Bool (Set (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i1")))) ; 
 
theorem :: JORDAN5B:2 (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "k"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i"))))) ; 
 
theorem :: JORDAN5B:3 (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set  "(" (Set (Var "k"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) ; 
 
theorem :: JORDAN5B:4 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) )))) "holds"  (Bool (Set (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "r")))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) )))) ; 
 
theorem :: JORDAN5B:5 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ))) "holds"  (Bool (Set (Var "p1"))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) ; 
 
theorem :: JORDAN5B:6 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ))) "holds"  (Bool (Set (Var "p1"))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) ; 
 
theorem :: JORDAN5B:7 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "P")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ) & (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (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 (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool  "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "p1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p2"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p1"))) & (Bool (Set (Var "p1"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p2"))) & (Bool (Set (Var "p2"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k1_rcomp_1 :::".]"::: ) ))) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" )))))) ; 
 
theorem :: JORDAN5B:8 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "Q")) "," (Set (Var "R")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "Q")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ) & (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 (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "F"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set (Var "i")) ")" )) & (Bool (Set (Var "Q"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set (Var "i")) ")" ))) "holds"  (Bool  "ex" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set (Var "P")) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "R")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "P")))) & (Bool (Set (Var "G")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )  ")" ))))))) ; 
 begin  
theorem :: JORDAN5B:9 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ))) "holds"  (Bool   ($#r2_jordan3 :::"LE"::: )  (Set (Var "p")) "," (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p2")))) ; 
 
theorem :: JORDAN5B:10 (Bool  "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ))) "holds"  (Bool   ($#r2_jordan3 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p2")))) ; 
 
theorem :: JORDAN5B:11 (Bool  "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2")))) "holds"  (Bool   ($#r2_jordan3 :::"LE"::: )  (Set (Var "p")) "," (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "p2")))) ; 
 
theorem :: JORDAN5B:12 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool   ($#r2_jordan3 :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool   ($#r2_jordan3 :::"LE"::: )  (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds"  (Bool   ($#r2_jordan3 :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q3")) "," (Set (Var "p1")) "," (Set (Var "p2")))) ; 
 
theorem :: JORDAN5B:13 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q")))) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p1")) where p1 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool   ($#r2_jordan3 :::"LE"::: )  (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "q"))) & (Bool   ($#r2_jordan3 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "q")))  ")" )  "}"  )) ; 
 
theorem :: JORDAN5B:14 (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"::: )  (Set (Var "n")) ")" )  (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 "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2")))) "holds"  (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p2")) "," (Set (Var "p1")))))) ; 
 
theorem :: JORDAN5B:15 (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set (Var "i")) ")" ))) "holds"  (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i"))) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))))) ; 
 begin  
theorem :: JORDAN5B:16 (Bool  "for" (Set (Var "g1")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_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 "g1")))) & (Bool (Set (Var "g1")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ) & (Bool (Set (Set (Var "g1"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "g1")) "," (Set (Var "i")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g1")) ")" ) ")"  ")" )))) "holds"  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: JORDAN5B:17 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "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 (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set   ($#k2_jordan3 :::"L_Cut"::: )   "(" (Set (Var "f")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))) ; 
 
theorem :: JORDAN5B:18 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "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 (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  )) "holds"  (Bool (Set   ($#k1_jordan3 :::"Index"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k2_jordan3 :::"L_Cut"::: )   "(" (Set (Var "f")) "," (Set (Var "p")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: JORDAN5B:19 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "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 (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k2_jordan3 :::"L_Cut"::: )   "(" (Set (Var "f")) "," (Set (Var "p")) ")"  ")" ))))) ; 
 
theorem :: JORDAN5B:20 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "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 (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1)))) "holds"  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k3_jordan3 :::"R_Cut"::: )   "(" (Set (Var "f")) "," (Set (Var "p")) ")"  ")" ))))) ; 
 
theorem :: JORDAN5B:21 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "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 (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set   ($#k4_jordan3 :::"B_Cut"::: )   "(" (Set (Var "f")) "," (Set (Var "p")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))) ; 
 
theorem :: JORDAN5B:22 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  )) "holds"  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k2_jordan3 :::"L_Cut"::: )   "(" (Set (Var "f")) "," (Set (Var "q")) ")"  ")" ))))) ; 
 
theorem :: JORDAN5B:23 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ) & (Bool (Bool  "not" (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k2_jordan3 :::"L_Cut"::: )   "(" (Set (Var "f")) "," (Set (Var "q")) ")"  ")" ))))) "holds"  (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k2_jordan3 :::"L_Cut"::: )   "(" (Set (Var "f")) "," (Set (Var "p")) ")"  ")" ))))) ; 
 
theorem :: JORDAN5B:24 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  )) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k4_jordan3 :::"B_Cut"::: )   "(" (Set (Var "f")) "," (Set (Var "p")) "," (Set (Var "q")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))))) ; 
 
theorem :: JORDAN5B:25 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set  "("  ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) ")"  ")" ) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "j")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) ")"  ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: JORDAN5B:26 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set  "("  ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) "," (Num 1) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set (Var "i")) ")"  ")" ) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set (Var "j")) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) ")"  ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: JORDAN5B:27 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  )) "holds"  (Bool (Set   ($#k2_jordan3 :::"L_Cut"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "f")))) ; 
 
theorem :: JORDAN5B:28 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  )) "holds"  (Bool (Set   ($#k3_jordan3 :::"R_Cut"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "f")))) ; 
 
theorem :: JORDAN5B:29 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "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 (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k1_jordan3 :::"Index"::: )   "(" (Set (Var "p")) "," (Set (Var "f")) ")"  ")" ) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set  "("  ($#k1_jordan3 :::"Index"::: )   "(" (Set (Var "p")) "," (Set (Var "f")) ")"  ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )))) ; 
 
theorem :: JORDAN5B:30 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_topreal1 :::"unfolded"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v3_topreal1 :::"s.n.c."::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set (Var "i")) ")" ))) "holds"  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: JORDAN5B:31 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "j")) "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) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set (Var "j")) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set (Var "j")) ")"  ")" ) ")" ))) "holds"  (Bool (Set (Var "P"))  ($#r1_topreal4 :::"is_S-P_arc_joining"::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set (Var "j")) ")" ) "," (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set (Var "j")) ")" ))))) ; 
 
theorem :: JORDAN5B:32 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "j")) "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) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "j")) "," (Num 1) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "j")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) ")"  ")" ) ")" ))) "holds"  (Bool (Set (Var "P"))  ($#r1_topreal4 :::"is_S-P_arc_joining"::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "j")) "," (Num 1) ")" ) "," (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "j")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: JORDAN5B:33 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool  "("  (Bool (Set   ($#k1_jordan3 :::"Index"::: )   "(" (Set (Var "p")) "," (Set (Var "f")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_jordan3 :::"Index"::: )   "(" (Set (Var "q")) "," (Set (Var "f")) ")" )) "or" (Bool  "("  (Bool (Set   ($#k1_jordan3 :::"Index"::: )   "(" (Set (Var "p")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_jordan3 :::"Index"::: )   "(" (Set (Var "q")) "," (Set (Var "f")) ")" )) & (Bool   ($#r2_jordan3 :::"LE"::: )  (Set (Var "p")) "," (Set (Var "q")) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k1_jordan3 :::"Index"::: )   "(" (Set (Var "p")) "," (Set (Var "f")) ")"  ")" )) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set  "("  ($#k1_jordan3 :::"Index"::: )   "(" (Set (Var "p")) "," (Set (Var "f")) ")"  ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" )  ")" ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q")))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k4_jordan3 :::"B_Cut"::: )   "(" (Set (Var "f")) "," (Set (Var "p")) "," (Set (Var "q")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))))) ;