:: JORDAN6 semantic presentation begin theorem :: JORDAN6:1 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s")))) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "r")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "s")) ")" ) ($#k6_real_1 :::"/"::: ) (Num 2))) & (Bool (Set (Set "(" (Set (Var "r")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "s")) ")" ) ($#k6_real_1 :::"/"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) ")" )) ; theorem :: JORDAN6:2 (Bool "for" (Set (Var "TX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TX")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "TX")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TX")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ))))) ; theorem :: JORDAN6:3 (Bool "for" (Set (Var "TX")) "," (Set (Var "TY")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TY")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "TX")) "," (Set "(" (Set (Var "TY")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "TX")) "," (Set (Var "TY"))) & (Bool "(" "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "TX")) "," (Set (Var "TY")) "st" (Bool (Bool (Set (Var "f2")) ($#r1_funct_2 :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Var "f2")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ) ")" )))) ; theorem :: JORDAN6:4 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (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_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: JORDAN6:5 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (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_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: JORDAN6:6 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (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_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: JORDAN6:7 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (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_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: JORDAN6:8 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (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_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: JORDAN6:9 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (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_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: JORDAN6:10 (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")) "is" ($#v2_connsp_1 :::"connected"::: ) )))) ; theorem :: JORDAN6:11 (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")) "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")))) "holds" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: JORDAN6:12 (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")) "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")))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2))) ")" )))) ; theorem :: JORDAN6:13 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "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 "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2))) "}" )) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Q"))) & (Bool (Set (Set (Var "P")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Q"))) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ))) ; theorem :: JORDAN6:14 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "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 "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2))) "}" )) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Q"))) & (Bool (Set (Set (Var "P")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Q"))) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ))) ; definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "p1", "p2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); func :::"x_Middle"::: "(" "P" "," "p1" "," "p2" ")" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) means :: JORDAN6:def 1 (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "p1" ($#k17_euclid :::"`1"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" "p2" ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2))) "}" )) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_jordan5c :::"First_Point"::: ) "(" "P" "," "p1" "," "p2" "," (Set (Var "Q")) ")" ))); end; :: deftheorem defines :::"x_Middle"::: JORDAN6:def 1 : (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 "b4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan6 :::"x_Middle"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) ")" )) "iff" (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2))) "}" )) "holds" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan5c :::"First_Point"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "Q")) ")" ))) ")" ))); definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "p1", "p2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); func :::"y_Middle"::: "(" "P" "," "p1" "," "p2" ")" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) means :: JORDAN6:def 2 (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "p1" ($#k18_euclid :::"`2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" "p2" ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2))) "}" )) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_jordan5c :::"First_Point"::: ) "(" "P" "," "p1" "," "p2" "," (Set (Var "Q")) ")" ))); end; :: deftheorem defines :::"y_Middle"::: JORDAN6:def 2 : (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 "b4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_jordan6 :::"y_Middle"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) ")" )) "iff" (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2))) "}" )) "holds" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan5c :::"First_Point"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "Q")) ")" ))) ")" ))); theorem :: JORDAN6:15 (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")) "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")))) "holds" (Bool "(" (Bool (Set ($#k1_jordan6 :::"x_Middle"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set ($#k2_jordan6 :::"y_Middle"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) ")" ))) ; theorem :: JORDAN6:16 (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")) "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")))) "holds" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan6 :::"x_Middle"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) ")" )) "iff" (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) )) ")" ))) ; theorem :: JORDAN6:17 (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")) "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")))) "holds" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set ($#k2_jordan6 :::"y_Middle"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) ")" )) "iff" (Bool (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) )) ")" ))) ; begin theorem :: JORDAN6:18 (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 ($#r1_jordan5c :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q2")) "," (Set (Var "q1")) "," (Set (Var "P")) "," (Set (Var "p2")) "," (Set (Var "p1"))))) ; definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "p1", "p2", "q1" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); func :::"L_Segment"::: "(" "P" "," "p1" "," "p2" "," "q1" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN6:def 3 "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q")) "," "q1" "," "P" "," "p1" "," "p2") "}" ; end; :: deftheorem defines :::"L_Segment"::: JORDAN6:def 3 : (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")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_jordan6 :::"L_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) "}" ))); definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "p1", "p2", "q1" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); func :::"R_Segment"::: "(" "P" "," "p1" "," "p2" "," "q1" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN6:def 4 "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool ($#r1_jordan5c :::"LE"::: ) "q1" "," (Set (Var "q")) "," "P" "," "p1" "," "p2") "}" ; end; :: deftheorem defines :::"R_Segment"::: JORDAN6:def 4 : (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")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k4_jordan6 :::"R_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) "}" ))); theorem :: JORDAN6:19 (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")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_jordan6 :::"L_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))))) ; theorem :: JORDAN6:20 (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")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k4_jordan6 :::"R_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))))) ; theorem :: JORDAN6:21 (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")) "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")))) "holds" (Bool (Set ($#k3_jordan6 :::"L_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "p1")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: JORDAN6:22 (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")) "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")))) "holds" (Bool (Set ($#k3_jordan6 :::"L_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "P"))))) ; theorem :: JORDAN6: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")) "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")))) "holds" (Bool (Set ($#k4_jordan6 :::"R_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "p2")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: JORDAN6:24 (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")) "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")))) "holds" (Bool (Set ($#k4_jordan6 :::"R_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "P"))))) ; theorem :: JORDAN6:25 (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")) "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")))) "holds" (Bool (Set ($#k4_jordan6 :::"R_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_jordan6 :::"L_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "q1")) ")" )))) ; definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "p1", "p2", "q1", "q2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); func :::"Segment"::: "(" "P" "," "p1" "," "p2" "," "q1" "," "q2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN6:def 5 (Set (Set "(" ($#k4_jordan6 :::"R_Segment"::: ) "(" "P" "," "p1" "," "p2" "," "q1" ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_jordan6 :::"L_Segment"::: ) "(" "P" "," "p1" "," "p2" "," "q2" ")" ")" )); end; :: deftheorem defines :::"Segment"::: JORDAN6:def 5 : (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) ")" ) "holds" (Bool (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_jordan6 :::"R_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_jordan6 :::"L_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q2")) ")" ")" ))))); theorem :: JORDAN6:26 (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) ")" ) "holds" (Bool (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q")) "," (Set (Var "q2")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) ")" ) "}" ))) ; theorem :: JORDAN6:27 (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 ($#r1_jordan5c :::"LE"::: ) (Set (Var "q2")) "," (Set (Var "q1")) "," (Set (Var "P")) "," (Set (Var "p2")) "," (Set (Var "p1")))) "holds" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))))) ; theorem :: JORDAN6:28 (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 "q")) "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")))) "holds" (Bool (Set ($#k3_jordan6 :::"L_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_jordan6 :::"R_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "q")) ")" )))) ; theorem :: JORDAN6:29 (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")))) "holds" (Bool (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "q2")) "," (Set (Var "q1")) ")" )))) ; begin definitionlet "s" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Vertical_Line"::: "s" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN6:def 6 "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) "s") "}" ; func :::"Horizontal_Line"::: "s" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN6:def 7 "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) "s") "}" ; end; :: deftheorem defines :::"Vertical_Line"::: JORDAN6:def 6 : (Bool "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_jordan6 :::"Vertical_Line"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) "}" )); :: deftheorem defines :::"Horizontal_Line"::: JORDAN6:def 7 : (Bool "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k7_jordan6 :::"Horizontal_Line"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) "}" )); theorem :: JORDAN6:30 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k6_jordan6 :::"Vertical_Line"::: ) (Set (Var "r"))) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set ($#k7_jordan6 :::"Horizontal_Line"::: ) (Set (Var "r"))) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )) ; theorem :: JORDAN6:31 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k6_jordan6 :::"Vertical_Line"::: ) (Set (Var "r")))) "iff" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" ))) ; theorem :: JORDAN6:32 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k7_jordan6 :::"Horizontal_Line"::: ) (Set (Var "r")))) "iff" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" ))) ; theorem :: JORDAN6:33 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) )) "holds" (Bool "ex" (Set (Var "P1")) "," (Set (Var "P2")) "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 "P1")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))) "," (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")))) & (Bool (Set (Var "P2")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P"))) "," (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) & (Bool (Set (Set (Var "P1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Set (Var "P1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k1_jordan5c :::"First_Point"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" ($#k2_jordan5c :::"Last_Point"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" ))) ; begin theorem :: JORDAN6:34 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) )) ($#k6_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) )))) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) )) ; theorem :: JORDAN6:35 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: JORDAN6:36 (Bool "for" (Set (Var "P7")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "P7")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) )) ($#k6_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "P7")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P7")) "is" ($#v2_connsp_1 :::"connected"::: ) ) ")" )) ; theorem :: JORDAN6:37 (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 "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))))) ; theorem :: JORDAN6:38 (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 "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (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"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) )))) "holds" (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) ))))) ; theorem :: JORDAN6:39 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (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 "P2")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "P1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "P1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P1")) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) )))) "holds" (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) ))))) ; theorem :: JORDAN6:40 (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 "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (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"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) )))) "holds" (Bool (Set (Var "Q")) "is" ($#v2_connsp_1 :::"connected"::: ) ))))) ; theorem :: JORDAN6:41 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P1")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "Q9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "GX")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P1")) ")" ) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "GX")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) "st" (Bool (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Var "Q9"))) & (Bool (Set (Var "Q9")) "is" ($#v2_connsp_1 :::"connected"::: ) )) "holds" (Bool (Set (Var "Q")) "is" ($#v2_connsp_1 :::"connected"::: ) ))))) ; theorem :: JORDAN6:42 (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 "ex" (Set (Var "p3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p3")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1"))) & (Bool (Set (Var "p3")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) ")" ))))) ; theorem :: JORDAN6:43 (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 (Set (Var "P")) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: JORDAN6:44 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P1")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (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 "P1")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P1")) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) )))) "holds" (Bool (Set (Var "Q")) "is" ($#v2_connsp_1 :::"connected"::: ) ))))) ; theorem :: JORDAN6:45 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "," (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "P2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set "(" (Set (Var "S")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P1")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "S")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P2")) ")" ) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "h")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))) & (Bool (Set (Var "h")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ))))))) ; theorem :: JORDAN6:46 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "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 "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 "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set (Var "P2")))))) ; theorem :: JORDAN6:47 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (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 "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ) & (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) )))) "holds" (Bool "not" (Bool (Set (Var "Q")) "is" ($#v2_connsp_1 :::"connected"::: ) ))))) ; theorem :: JORDAN6:48 (Bool "for" (Set (Var "P")) "," (Set (Var "P1")) "," (Set (Var "P2")) "," (Set (Var "P19")) "," (Set (Var "P29")) "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 "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ) & (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 (Set (Var "P1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Var "P19")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P29")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "P19")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "P29"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool "not" (Bool "(" (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set (Var "P19"))) & (Bool (Set (Var "P2")) ($#r1_hidden :::"="::: ) (Set (Var "P29"))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set (Var "P29"))) & (Bool (Set (Var "P2")) ($#r1_hidden :::"="::: ) (Set (Var "P19"))) ")" ))) ; begin theorem :: JORDAN6:49 (Bool "for" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (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 (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Var "P1")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool "(" (Bool (Set (Var "P1")) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k6_jordan6 :::"Vertical_Line"::: ) (Set (Var "r")))) & (Bool (Set (Set (Var "P1")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set (Var "r")) ")" )) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )))) ; definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); assume (Bool (Set (Const "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ) ; func :::"Upper_Arc"::: "P" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) means :: JORDAN6:def 8 (Bool "(" (Bool it ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) "P") "," (Set ($#k22_pscomp_1 :::"E-max"::: ) "P")) & (Bool "ex" (Set (Var "P2")) "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 "P2")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) "P") "," (Set ($#k18_pscomp_1 :::"W-min"::: ) "P")) & (Bool (Set it ($#k9_subset_1 :::"/\"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) "P" ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) "P" ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set it ($#k4_subset_1 :::"\/"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) "P") & (Bool (Set (Set "(" ($#k1_jordan5c :::"First_Point"::: ) "(" it "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) "P" ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) "P" ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) "P" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) "P" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" ($#k2_jordan5c :::"Last_Point"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) "P" ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) "P" ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) "P" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) "P" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" )) ")" ); end; :: deftheorem defines :::"Upper_Arc"::: JORDAN6:def 8 : (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")))) "iff" (Bool "(" (Bool (Set (Var "b2")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))) "," (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")))) & (Bool "ex" (Set (Var "P2")) "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 "P2")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P"))) "," (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) & (Bool (Set (Set (Var "b2")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Set (Var "b2")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k1_jordan5c :::"First_Point"::: ) "(" (Set (Var "b2")) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" ($#k2_jordan5c :::"Last_Point"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" )) ")" ) ")" ))); definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); assume (Bool (Set (Const "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ) ; func :::"Lower_Arc"::: "P" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) means :: JORDAN6:def 9 (Bool "(" (Bool it ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) "P") "," (Set ($#k18_pscomp_1 :::"W-min"::: ) "P")) & (Bool (Set (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) "P" ")" ) ($#k9_subset_1 :::"/\"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) "P" ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) "P" ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) "P" ")" ) ($#k4_subset_1 :::"\/"::: ) it) ($#r1_hidden :::"="::: ) "P") & (Bool (Set (Set "(" ($#k1_jordan5c :::"First_Point"::: ) "(" (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) "P" ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) "P" ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) "P" ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) "P" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) "P" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" ($#k2_jordan5c :::"Last_Point"::: ) "(" it "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) "P" ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) "P" ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) "P" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) "P" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" ); end; :: deftheorem defines :::"Lower_Arc"::: JORDAN6:def 9 : (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")))) "iff" (Bool "(" (Bool (Set (Var "b2")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P"))) "," (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) & (Bool (Set (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k1_jordan5c :::"First_Point"::: ) "(" (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" ($#k2_jordan5c :::"Last_Point"::: ) "(" (Set (Var "b2")) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" ) ")" ))); theorem :: JORDAN6:50 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) )) "holds" (Bool "(" (Bool (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P"))) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))) "," (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")))) & (Bool (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P"))) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P"))) "," (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) & (Bool (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P"))) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P"))) "," (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) & (Bool (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P"))) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))) "," (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")))) & (Bool (Set (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k1_jordan5c :::"First_Point"::: ) "(" (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" ($#k2_jordan5c :::"Last_Point"::: ) "(" (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" )) ; theorem :: JORDAN6:51 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) )) "holds" (Bool "(" (Bool (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) ($#k2_tarski :::"}"::: ) ))) & (Bool (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) ($#k2_tarski :::"}"::: ) ))) ")" )) ; theorem :: JORDAN6:52 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ) & (Bool (Set (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "P1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "P1"))) ($#r1_hidden :::"="::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")))))) ; theorem :: JORDAN6:53 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ) & (Bool (Set (Set (Var "P1")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Set (Var "P1")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")))))) ; begin theorem :: JORDAN6:54 (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 "q")) "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 ($#r1_jordan5c :::"LE"::: ) (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))))) ; theorem :: JORDAN6:55 (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 "q")) "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 ($#r1_jordan5c :::"LE"::: ) (Set (Var "p2")) "," (Set (Var "q")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))))) ; definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "q1", "q2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); pred :::"LE"::: "q1" "," "q2" "," "P" means :: JORDAN6:def 10 (Bool "(" (Bool "(" (Bool "q1" ($#r2_hidden :::"in"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) "P")) & (Bool "q2" ($#r2_hidden :::"in"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) "P")) & (Bool (Bool "not" "q2" ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) "P"))) ")" ) "or" (Bool "(" (Bool "q1" ($#r2_hidden :::"in"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) "P")) & (Bool "q2" ($#r2_hidden :::"in"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) "P")) & (Bool ($#r1_jordan5c :::"LE"::: ) "q1" "," "q2" "," (Set ($#k8_jordan6 :::"Upper_Arc"::: ) "P") "," (Set ($#k18_pscomp_1 :::"W-min"::: ) "P") "," (Set ($#k22_pscomp_1 :::"E-max"::: ) "P")) ")" ) "or" (Bool "(" (Bool "q1" ($#r2_hidden :::"in"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) "P")) & (Bool "q2" ($#r2_hidden :::"in"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) "P")) & (Bool (Bool "not" "q2" ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) "P"))) & (Bool ($#r1_jordan5c :::"LE"::: ) "q1" "," "q2" "," (Set ($#k9_jordan6 :::"Lower_Arc"::: ) "P") "," (Set ($#k22_pscomp_1 :::"E-max"::: ) "P") "," (Set ($#k18_pscomp_1 :::"W-min"::: ) "P")) ")" ) ")" ); end; :: deftheorem defines :::"LE"::: JORDAN6:def 10 : (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P"))) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")))) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")))) & (Bool (Bool "not" (Set (Var "q2")) ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))))) ")" ) "or" (Bool "(" (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")))) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P"))) "," (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))) "," (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")))) ")" ) "or" (Bool "(" (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")))) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")))) & (Bool (Bool "not" (Set (Var "q2")) ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P"))) "," (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P"))) "," (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) ")" ) ")" ) ")" ))); theorem :: JORDAN6:56 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q")) "," (Set (Var "q")) "," (Set (Var "P"))))) ; theorem :: JORDAN6:57 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (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")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ) & (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P"))) & (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q2")) "," (Set (Var "q1")) "," (Set (Var "P")))) "holds" (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Var "q2"))))) ; theorem :: JORDAN6:58 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (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 "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ) & (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P"))) & (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "P")))) "holds" (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q3")) "," (Set (Var "P"))))) ; theorem :: JORDAN6:59 (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 "q")) "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 "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool "not" (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_jordan6 :::"L_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) ")" ))))) ; theorem :: JORDAN6:60 (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 "q")) "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 "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1")))) "holds" (Bool "not" (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_jordan6 :::"R_Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) ")" ))))) ; registrationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k9_jordan6 :::"Lower_Arc"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ; cluster (Set ($#k8_jordan6 :::"Upper_Arc"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ; end; theorem :: JORDAN6:61 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) & (Bool (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) ")" )) ; definitionlet "C" be ($#m1_subset_1 :::"Simple_closed_curve":::); func :::"Lower_Middle_Point"::: "C" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN6:def 11 (Set ($#k1_jordan5c :::"First_Point"::: ) "(" (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) "C" ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) "C" ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) "C" ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) "C" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) "C" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ); func :::"Upper_Middle_Point"::: "C" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN6:def 12 (Set ($#k1_jordan5c :::"First_Point"::: ) "(" (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) "C" ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) "C" ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) "C" ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) "C" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) "C" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Lower_Middle_Point"::: JORDAN6:def 11 : (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k10_jordan6 :::"Lower_Middle_Point"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan5c :::"First_Point"::: ) "(" (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))); :: deftheorem defines :::"Upper_Middle_Point"::: JORDAN6:def 12 : (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k11_jordan6 :::"Upper_Middle_Point"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan5c :::"First_Point"::: ) "(" (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))); theorem :: JORDAN6:62 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )))) ; theorem :: JORDAN6:63 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )))) ; theorem :: JORDAN6:64 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set (Set "(" ($#k10_jordan6 :::"Lower_Middle_Point"::: ) (Set (Var "C")) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))) ; theorem :: JORDAN6:65 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set (Set "(" ($#k11_jordan6 :::"Upper_Middle_Point"::: ) (Set (Var "C")) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))) ; theorem :: JORDAN6:66 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k10_jordan6 :::"Lower_Middle_Point"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C"))))) ; theorem :: JORDAN6:67 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k11_jordan6 :::"Upper_Middle_Point"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C"))))) ; theorem :: JORDAN6:68 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k11_jordan6 :::"Upper_Middle_Point"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) ; theorem :: JORDAN6:69 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set "(" ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C")) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set "(" ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C")) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")))))) ; theorem :: JORDAN6:70 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set "(" ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C")) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set "(" ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C")) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")))))) ;