:: JORDAN16  semantic presentation begin  



















theorem :: JORDAN16:1 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  "holds" (Bool (Set   ($#k9_jordan6 :::"Lower_Arc"::: )  (Set (Var "C")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k8_jordan6 :::"Upper_Arc"::: )  (Set (Var "C"))))) ; 
 
theorem :: JORDAN16:2 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k5_jordan6 :::"Segment"::: )   "(" (Set (Var "A")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "A"))))) ; 
 
theorem :: JORDAN16:3 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_jordan6 :::"L_Segment"::: )   "(" (Set (Var "A")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) ")" )))) ; 
 
theorem :: JORDAN16:4 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_jordan6 :::"R_Segment"::: )   "(" (Set (Var "A")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) ")" )))) ; 
 
theorem :: JORDAN16:5 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool   ($#r1_jordan5c :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "A")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds"  (Bool  "("  (Bool (Set (Var "q1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_jordan6 :::"Segment"::: )   "(" (Set (Var "A")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" )) & (Bool (Set (Var "q2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_jordan6 :::"Segment"::: )   "(" (Set (Var "A")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" ))  ")" ))) ; 
 
theorem :: JORDAN16:6 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k1_jordan7 :::"Segment"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "C")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "C"))))) ; 
 
theorem :: JORDAN16:7 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (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 (Var "C"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Bool  "not"   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "C"))))) "holds"  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "C"))))) ; 
 
theorem :: JORDAN16:8 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y0")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "Y"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y0"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))))) ; 
 
theorem :: JORDAN16:9 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "S0")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "S"))  (Bool  "for" (Set (Var "T0")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )) "holds"  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S0")) "," (Set (Var "T0"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k2_tmap_1 :::"|"::: )  (Set (Var "S0")))) & (Bool (Set (Var "g")) "is"   ($#v2_funct_2 :::"onto"::: )  )) "holds"  (Bool (Set (Var "g")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )))))) ; 
 
theorem :: JORDAN16:10 (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "," (Set (Var "P3")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P1"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P2"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P3"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "P2"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "P3")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "P1"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "P2"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "P3")))) & (Bool (Bool  "not" (Set (Var "P1"))  ($#r1_hidden :::"="::: )  (Set (Var "P2"))))) "holds"  (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )  (Set (Var "P3"))))) ; 
 
theorem :: JORDAN16:11 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "A1"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "A2"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "A1"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))) & (Bool (Set (Var "A2"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))) & (Bool (Set (Var "A1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A2")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "A1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "A2")))  ($#r1_hidden :::"="::: )  (Set (Var "C"))) & (Bool (Set (Set (Var "A1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "A2")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) ))  ")" )))) ; 
 
theorem :: JORDAN16:12 (Bool  "for" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "A1"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "A1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "A2")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "q1")) "," (Set (Var "q2")) ($#k2_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "A1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A2"))))) ; 
 
theorem :: JORDAN16:13 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "A1"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "A2"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "A1"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))) & (Bool (Set (Var "A2"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))) & (Bool (Set (Set (Var "A1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "A2")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Set (Var "A1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "A2")))  ($#r1_hidden :::"="::: )  (Set (Var "C")))))) ; 
 
theorem :: JORDAN16:14 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "A1"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))) & (Bool (Set (Var "A2"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))) & (Bool (Set (Var "A1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A2"))) & (Bool (Set (Var "A1"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "A2"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2")))) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))) & (Bool (Bool  "not" (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "A1"))))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "A2"))))))) ; 
 
theorem :: JORDAN16:15 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "C"))) "," (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set (Var "C")))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))) & (Bool (Bool  "not" (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_jordan6 :::"Lower_Arc"::: )  (Set (Var "C")))))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_jordan6 :::"Upper_Arc"::: )  (Set (Var "C")))))) ; 
 
theorem :: JORDAN16:16 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool   ($#r1_jordan5c :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "A")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )(Bool  "ex" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "g")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p1"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p2"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set (Var "q1"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s2")))  ($#r1_hidden :::"="::: )  (Set (Var "q2"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s1"))) & (Bool (Set (Var "s1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s2"))) & (Bool (Set (Var "s2"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" ))))) ; 
 
theorem :: JORDAN16:17 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool   ($#r1_jordan5c :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "A")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q2")))) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )(Bool  "ex" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "g")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p1"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p2"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set (Var "q1"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s2")))  ($#r1_hidden :::"="::: )  (Set (Var "q2"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s1"))) & (Bool (Set (Var "s1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s2"))) & (Bool (Set (Var "s2"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" ))))) ; 
 
theorem :: JORDAN16:18 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool   ($#r1_jordan5c :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "A")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds"  (Bool  "not" (Bool (Set   ($#k5_jordan6 :::"Segment"::: )   "(" (Set (Var "A")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )))) ; 
 
theorem :: JORDAN16:19 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (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 (Var "C")))) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_jordan7 :::"Segment"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "C")) ")" ) "," (Set (Var "C")) ")" )) & (Bool (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_jordan7 :::"Segment"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "C")) ")" ) "," (Set (Var "C")) ")" ))  ")" ))) ; 
 
theorem :: JORDAN16:20 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set   ($#k1_fcont_1 :::"AffineMap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))) ; 
 
theorem :: JORDAN16:21 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool   ($#r1_jordan5c :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "A")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q2")))) "holds"  (Bool (Set   ($#k5_jordan6 :::"Segment"::: )   "(" (Set (Var "A")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" )  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "q1")) "," (Set (Var "q2"))))) ; 
 
theorem :: JORDAN16:22 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "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 "P"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))) & (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Bool  "not" (Set   ($#k8_jordan6 :::"Upper_Arc"::: )  (Set (Var "C")))  ($#r1_tarski :::"c="::: )  (Set (Var "P"))))) "holds"  (Bool (Set   ($#k9_jordan6 :::"Lower_Arc"::: )  (Set (Var "C")))  ($#r1_tarski :::"c="::: )  (Set (Var "P")))))) ; 
 
theorem :: JORDAN16:23 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "q1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "q2"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p1"))) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p1"))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q2")))) "holds"  (Bool  "ex" (Set (Var "Q")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "Q"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "q1")) "," (Set (Var "q2"))) & (Bool (Set (Var "Q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P"))) & (Bool (Set (Var "Q"))  ($#r1_subset_1 :::"misses"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) ))  ")" )))) ; 
 
theorem :: JORDAN16:24 (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 "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "q1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q1")))) "holds"  (Bool (Set   ($#k5_jordan6 :::"Segment"::: )   "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "q1")) ")" )  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "q1"))))) ;