:: JORDAN17  semantic presentation begin  











theorem :: JORDAN17:1 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "p1")) "," (Set (Var "p2")) "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 "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2")))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "P")) ")" )(Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (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"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )))))) ; 
 
theorem :: JORDAN17:2 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::) "holds"  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "P"))) "," (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set (Var "P"))) "," (Set (Var "P")))) ; 
 
theorem :: JORDAN17:3 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "a")) "," (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set (Var "P"))) "," (Set (Var "P")))) "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_jordan6 :::"Upper_Arc"::: )  (Set (Var "P")))))) ; 
 
theorem :: JORDAN17:4 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool   ($#r1_jordan6 :::"LE"::: )  (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set (Var "P"))) "," (Set (Var "a")) "," (Set (Var "P")))) "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_jordan6 :::"Lower_Arc"::: )  (Set (Var "P")))))) ; 
 
theorem :: JORDAN17:5 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "a")) "," (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "P"))) "," (Set (Var "P")))) "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_jordan6 :::"Lower_Arc"::: )  (Set (Var "P")))))) ; 
 
theorem :: JORDAN17:6 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "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 "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool   ($#r1_jordan5c :::"LE"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "P")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool   ($#r1_jordan5c :::"LE"::: )  (Set (Var "a")) "," (Set (Var "e")) "," (Set (Var "P")) "," (Set (Var "c")) "," (Set (Var "d"))) & (Bool   ($#r1_jordan5c :::"LE"::: )  (Set (Var "e")) "," (Set (Var "b")) "," (Set (Var "P")) "," (Set (Var "c")) "," (Set (Var "d")))  ")" )))) ; 
 
theorem :: JORDAN17:7 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "a")) "," (Set (Var "e")) "," (Set (Var "P")))  ")" )))) ; 
 
theorem :: JORDAN17:8 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "P")))  ")" )))) ; 
 definitionlet "P" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); let "a", "b", "c", "d" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); pred "a" "," "b" "," "c" "," "d" :::"are_in_this_order_on"::: "P" means :: JORDAN17:def 1 (Bool  "("  (Bool  "("  (Bool   ($#r1_jordan6 :::"LE"::: )  "a" "," "b" "," "P") & (Bool   ($#r1_jordan6 :::"LE"::: )  "b" "," "c" "," "P") & (Bool   ($#r1_jordan6 :::"LE"::: )  "c" "," "d" "," "P")  ")" ) "or" (Bool  "("  (Bool   ($#r1_jordan6 :::"LE"::: )  "b" "," "c" "," "P") & (Bool   ($#r1_jordan6 :::"LE"::: )  "c" "," "d" "," "P") & (Bool   ($#r1_jordan6 :::"LE"::: )  "d" "," "a" "," "P")  ")" ) "or" (Bool  "("  (Bool   ($#r1_jordan6 :::"LE"::: )  "c" "," "d" "," "P") & (Bool   ($#r1_jordan6 :::"LE"::: )  "d" "," "a" "," "P") & (Bool   ($#r1_jordan6 :::"LE"::: )  "a" "," "b" "," "P")  ")" ) "or" (Bool  "("  (Bool   ($#r1_jordan6 :::"LE"::: )  "d" "," "a" "," "P") & (Bool   ($#r1_jordan6 :::"LE"::: )  "a" "," "b" "," "P") & (Bool   ($#r1_jordan6 :::"LE"::: )  "b" "," "c" "," "P")  ")" )  ")" ); end; 








:: deftheorem    defines :::"are_in_this_order_on"::: JORDAN17:def 1 :  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P"))) "iff" (Bool  "("  (Bool  "("  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "P")))  ")" ) "or" (Bool  "("  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "P")))  ")" ) "or" (Bool  "("  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "P")))  ")" ) "or" (Bool  "("  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "P")))  ")" )  ")" )  ")" ))); 
 
theorem :: JORDAN17:9 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "a"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P"))))) ; 
 
theorem :: JORDAN17:10 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P"))))) ; 
 
theorem :: JORDAN17:11 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P"))))) ; 
 
theorem :: JORDAN17:12 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P"))))) ; 
 
theorem :: JORDAN17:13 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "e")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))  ")" )))) ; 
 
theorem :: JORDAN17:14 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "e")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))  ")" )))) ; 
 
theorem :: JORDAN17:15 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "e")) "," (Set (Var "c"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))  ")" )))) ; 
 
theorem :: JORDAN17:16 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "e")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))  ")" )))) ; 
 
theorem :: JORDAN17:17 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "e")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))  ")" )))) ; 
 
theorem :: JORDAN17:18 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "e")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))  ")" )))) ; 
 
theorem :: JORDAN17:19 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "e"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))  ")" )))) ; 
 
theorem :: JORDAN17:20 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))  ")" )))) ; 
 
theorem :: JORDAN17:21 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))) ; 
 
theorem :: JORDAN17:22 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P"))) & (Bool (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))))) ; 
 
theorem :: JORDAN17:23 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P"))) & (Bool (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "d"))))) ; 
 
theorem :: JORDAN17:24 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))))) ; 
 
theorem :: JORDAN17:25 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P"))) & (Bool (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "d"))))) ; 
 
theorem :: JORDAN17:26 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "c"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Var "d"))))) ; 
 
theorem :: JORDAN17:27 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "C")))) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "c"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "C")))) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "C")))) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "b"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "C")))) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r1_jordan17 :::"are_in_this_order_on"::: )  (Set (Var "C"))))) ;