:: JORDAN7 semantic presentation begin theorem :: JORDAN7:1 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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 ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")))) & (Bool (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")))) & (Bool (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")))) & (Bool (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")))) ")" )) ; theorem :: JORDAN7:2 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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 ($#r1_jordan6 :::"LE"::: ) (Set (Var "q")) "," (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))) "," (Set (Var "P")))) "holds" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))))) ; theorem :: JORDAN7:3 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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 ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))) "," (Set (Var "q")) "," (Set (Var "P"))))) ; definitionlet "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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) ")" ); func :::"Segment"::: "(" "q1" "," "q2" "," "P" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN7:def 1 "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool ($#r1_jordan6 :::"LE"::: ) "q1" "," (Set (Var "p")) "," "P") & (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "p")) "," "q2" "," "P") ")" ) "}" if (Bool "q2" ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) "P")) otherwise "{" (Set (Var "p1")) where p1 "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool ($#r1_jordan6 :::"LE"::: ) "q1" "," (Set (Var "p1")) "," "P") "or" (Bool "(" (Bool "q1" ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) "P")) ")" ) ")" ) "}" ; end; :: deftheorem defines :::"Segment"::: JORDAN7:def 1 : (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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 (Bool (Set (Var "q2")) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))))) "implies" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "p")) "," (Set (Var "P"))) & (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "p")) "," (Set (Var "q2")) "," (Set (Var "P"))) ")" ) "}" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "q2")) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))))) "implies" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p1")) where p1 "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "p1")) "," (Set (Var "P"))) "or" (Bool "(" (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) ")" ) ")" ) "}" ) ")" ")" ))); theorem :: JORDAN7:4 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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 ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "P")))) & (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "P")))) ")" )) ; theorem :: JORDAN7:5 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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")))) "holds" (Bool "(" (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) ")" ))) ; theorem :: JORDAN7:6 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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")))) "holds" (Bool "(" (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) ")" )) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) ")" )) ")" ))) ; theorem :: JORDAN7:7 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "q1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) )) "holds" (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q1")) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set (Var "P")) ")" )))) ; theorem :: JORDAN7:8 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q")) "," (Set (Var "q")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "q")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: JORDAN7:9 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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 (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) & (Bool (Set (Var "q2")) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))))) "holds" (Bool "not" (Bool (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) ")" ))))) ; theorem :: JORDAN7:10 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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"))) & (Bool "(" "not" (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Var "q2"))) "or" "not" (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) ")" ) & (Bool "(" "not" (Bool (Set (Var "q2")) ($#r1_hidden :::"="::: ) (Set (Var "q3"))) "or" "not" (Bool (Set (Var "q2")) ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) ")" )) "holds" (Bool (Set (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "P")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "q2")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: JORDAN7:11 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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 (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) & (Bool (Set (Var "q2")) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q2")) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set (Var "P")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "q2")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: JORDAN7:12 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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 (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q2")) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set (Var "P")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set (Var "q1")) "," (Set (Var "P")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: JORDAN7:13 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "q4")) "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"))) & (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q3")) "," (Set (Var "q4")) "," (Set (Var "P"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "q2")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3")))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q3")) "," (Set (Var "q4")) "," (Set (Var "P")) ")" )))) ; theorem :: JORDAN7:14 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) & (Bool (Set (Var "q2")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3")))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q3")) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")) ")" ) "," (Set (Var "P")) ")" )))) ; begin theorem :: JORDAN7:15 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ))))) ; theorem :: JORDAN7:16 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "P")))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) ")" ))))) ; theorem :: JORDAN7: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")) "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")))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (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"))) ")" )))) ; theorem :: JORDAN7:18 (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")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (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 ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s1"))) & (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (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 "s2"))) & (Bool (Set (Var "s2")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2")))) "holds" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))))))) ; theorem :: JORDAN7:19 (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")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (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 ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s1"))) & (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (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 "s2"))) & (Bool (Set (Var "s2")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))))))) ; theorem :: JORDAN7:20 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ) & (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "st" (Bool "(" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P")))) & (Bool (Set (Var "h")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Num 8) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h"))))) "holds" (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) "," (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," (Set (Var "P"))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "P")) ")" ))) "holds" (Bool (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set (Var "W"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))) ")" ) & (Bool "(" "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set (Var "P")) ")" ))) "holds" (Bool (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set (Var "W"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "P")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) "," (Set (Var "P")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )) ")" ) & (Bool (Set (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set (Var "P")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) "," (Set (Var "P")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" ) ")" ) "," (Set (Var "P")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set (Var "P")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" ) ")" ) "," (Set (Var "P")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) "," (Set (Var "P")) ")" )) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Bool "not" (Set (Var "i")) "," (Set (Var "j")) ($#r1_gobrd10 :::"are_adjacent1"::: ) ))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "P")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "P")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h"))))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set (Var "P")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "P")) ")" )) ")" ) ")" )))) ;