:: JORDAN20 semantic presentation begin theorem :: JORDAN20: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 "p")) "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 "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: JORDAN20:2 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))))) ; theorem :: JORDAN20:3 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "a"))))) ; theorem :: JORDAN20:4 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))))) ; theorem :: JORDAN20:5 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a"))))) ; theorem :: JORDAN20:6 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"S-Sequence_in_R2":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "j")) ")" )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ))))) ; theorem :: JORDAN20:7 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"S-Sequence_in_R2":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "j")) ")" )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ))))) ; definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "p1", "p2", "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "e" be ($#m1_subset_1 :::"Real":::); pred "p" :::"is_Lin"::: "P" "," "p1" "," "p2" "," "e" means :: JORDAN20:def 1 (Bool "(" (Bool "P" ($#r1_topreal1 :::"is_an_arc_of"::: ) "p1" "," "p2") & (Bool "p" ($#r2_hidden :::"in"::: ) "P") & (Bool (Set "p" ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) "e") & (Bool "ex" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "p4")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) "e") & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," "p" "," "P" "," "p1" "," "p2") & (Bool "(" "for" (Set (Var "p5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," (Set (Var "p5")) "," "P" "," "p1" "," "p2") & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p5")) "," "p" "," "P" "," "p1" "," "p2")) "holds" (Bool (Set (Set (Var "p5")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) "e") ")" ) ")" )) ")" ); pred "p" :::"is_Rin"::: "P" "," "p1" "," "p2" "," "e" means :: JORDAN20:def 2 (Bool "(" (Bool "P" ($#r1_topreal1 :::"is_an_arc_of"::: ) "p1" "," "p2") & (Bool "p" ($#r2_hidden :::"in"::: ) "P") & (Bool (Set "p" ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) "e") & (Bool "ex" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "p4")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) "e") & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," "p" "," "P" "," "p1" "," "p2") & (Bool "(" "for" (Set (Var "p5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," (Set (Var "p5")) "," "P" "," "p1" "," "p2") & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p5")) "," "p" "," "P" "," "p1" "," "p2")) "holds" (Bool (Set (Set (Var "p5")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) "e") ")" ) ")" )) ")" ); pred "p" :::"is_Lout"::: "P" "," "p1" "," "p2" "," "e" means :: JORDAN20:def 3 (Bool "(" (Bool "P" ($#r1_topreal1 :::"is_an_arc_of"::: ) "p1" "," "p2") & (Bool "p" ($#r2_hidden :::"in"::: ) "P") & (Bool (Set "p" ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) "e") & (Bool "ex" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "p4")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) "e") & (Bool ($#r1_jordan5c :::"LE"::: ) "p" "," (Set (Var "p4")) "," "P" "," "p1" "," "p2") & (Bool "(" "for" (Set (Var "p5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p5")) "," (Set (Var "p4")) "," "P" "," "p1" "," "p2") & (Bool ($#r1_jordan5c :::"LE"::: ) "p" "," (Set (Var "p5")) "," "P" "," "p1" "," "p2")) "holds" (Bool (Set (Set (Var "p5")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) "e") ")" ) ")" )) ")" ); pred "p" :::"is_Rout"::: "P" "," "p1" "," "p2" "," "e" means :: JORDAN20:def 4 (Bool "(" (Bool "P" ($#r1_topreal1 :::"is_an_arc_of"::: ) "p1" "," "p2") & (Bool "p" ($#r2_hidden :::"in"::: ) "P") & (Bool (Set "p" ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) "e") & (Bool "ex" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "p4")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) "e") & (Bool ($#r1_jordan5c :::"LE"::: ) "p" "," (Set (Var "p4")) "," "P" "," "p1" "," "p2") & (Bool "(" "for" (Set (Var "p5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p5")) "," (Set (Var "p4")) "," "P" "," "p1" "," "p2") & (Bool ($#r1_jordan5c :::"LE"::: ) "p" "," (Set (Var "p5")) "," "P" "," "p1" "," "p2")) "holds" (Bool (Set (Set (Var "p5")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) "e") ")" ) ")" )) ")" ); pred "p" :::"is_OSin"::: "P" "," "p1" "," "p2" "," "e" means :: JORDAN20:def 5 (Bool "(" (Bool "P" ($#r1_topreal1 :::"is_an_arc_of"::: ) "p1" "," "p2") & (Bool "p" ($#r2_hidden :::"in"::: ) "P") & (Bool (Set "p" ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) "e") & (Bool "ex" (Set (Var "p7")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p7")) "," "p" "," "P" "," "p1" "," "p2") & (Bool "(" "for" (Set (Var "p8")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p7")) "," (Set (Var "p8")) "," "P" "," "p1" "," "p2") & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p8")) "," "p" "," "P" "," "p1" "," "p2")) "holds" (Bool (Set (Set (Var "p8")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) "e") ")" ) & (Bool "(" "for" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," (Set (Var "p7")) "," "P" "," "p1" "," "p2") & (Bool (Set (Var "p4")) ($#r1_hidden :::"<>"::: ) (Set (Var "p7")))) "holds" (Bool "(" (Bool "ex" (Set (Var "p5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," (Set (Var "p5")) "," "P" "," "p1" "," "p2") & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p5")) "," (Set (Var "p7")) "," "P" "," "p1" "," "p2") & (Bool (Set (Set (Var "p5")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) "e") ")" )) & (Bool "ex" (Set (Var "p6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," (Set (Var "p6")) "," "P" "," "p1" "," "p2") & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p6")) "," (Set (Var "p7")) "," "P" "," "p1" "," "p2") & (Bool (Set (Set (Var "p6")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) "e") ")" )) ")" ) ")" ) ")" )) ")" ); pred "p" :::"is_OSout"::: "P" "," "p1" "," "p2" "," "e" means :: JORDAN20:def 6 (Bool "(" (Bool "P" ($#r1_topreal1 :::"is_an_arc_of"::: ) "p1" "," "p2") & (Bool "p" ($#r2_hidden :::"in"::: ) "P") & (Bool (Set "p" ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) "e") & (Bool "ex" (Set (Var "p7")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) "p" "," (Set (Var "p7")) "," "P" "," "p1" "," "p2") & (Bool "(" "for" (Set (Var "p8")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p8")) "," (Set (Var "p7")) "," "P" "," "p1" "," "p2") & (Bool ($#r1_jordan5c :::"LE"::: ) "p" "," (Set (Var "p8")) "," "P" "," "p1" "," "p2")) "holds" (Bool (Set (Set (Var "p8")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) "e") ")" ) & (Bool "(" "for" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p7")) "," (Set (Var "p4")) "," "P" "," "p1" "," "p2") & (Bool (Set (Var "p4")) ($#r1_hidden :::"<>"::: ) (Set (Var "p7")))) "holds" (Bool "(" (Bool "ex" (Set (Var "p5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p5")) "," (Set (Var "p4")) "," "P" "," "p1" "," "p2") & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p7")) "," (Set (Var "p5")) "," "P" "," "p1" "," "p2") & (Bool (Set (Set (Var "p5")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) "e") ")" )) & (Bool "ex" (Set (Var "p6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p6")) "," (Set (Var "p4")) "," "P" "," "p1" "," "p2") & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p7")) "," (Set (Var "p6")) "," "P" "," "p1" "," "p2") & (Bool (Set (Set (Var "p6")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) "e") ")" )) ")" ) ")" ) ")" )) ")" ); end; :: deftheorem defines :::"is_Lin"::: JORDAN20: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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_jordan20 :::"is_Lin"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))) "iff" (Bool "(" (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool "ex" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "p4")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," (Set (Var "p")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool "(" "for" (Set (Var "p5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p5")) "," (Set (Var "p")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Set (Var "p5")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "e"))) ")" ) ")" )) ")" ) ")" )))); :: deftheorem defines :::"is_Rin"::: JORDAN20: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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_jordan20 :::"is_Rin"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))) "iff" (Bool "(" (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool "ex" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "p4")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "e"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," (Set (Var "p")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool "(" "for" (Set (Var "p5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p5")) "," (Set (Var "p")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Set (Var "p5")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "e"))) ")" ) ")" )) ")" ) ")" )))); :: deftheorem defines :::"is_Lout"::: JORDAN20: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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_jordan20 :::"is_Lout"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))) "iff" (Bool "(" (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool "ex" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "p4")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p")) "," (Set (Var "p4")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool "(" "for" (Set (Var "p5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p5")) "," (Set (Var "p4")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p")) "," (Set (Var "p5")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Set (Var "p5")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "e"))) ")" ) ")" )) ")" ) ")" )))); :: deftheorem defines :::"is_Rout"::: JORDAN20: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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r4_jordan20 :::"is_Rout"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))) "iff" (Bool "(" (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool "ex" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "p4")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "e"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p")) "," (Set (Var "p4")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool "(" "for" (Set (Var "p5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p5")) "," (Set (Var "p4")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p")) "," (Set (Var "p5")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Set (Var "p5")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "e"))) ")" ) ")" )) ")" ) ")" )))); :: deftheorem defines :::"is_OSin"::: JORDAN20: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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r5_jordan20 :::"is_OSin"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))) "iff" (Bool "(" (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool "ex" (Set (Var "p7")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p7")) "," (Set (Var "p")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool "(" "for" (Set (Var "p8")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p7")) "," (Set (Var "p8")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p8")) "," (Set (Var "p")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Set (Var "p8")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" ) & (Bool "(" "for" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," (Set (Var "p7")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "p4")) ($#r1_hidden :::"<>"::: ) (Set (Var "p7")))) "holds" (Bool "(" (Bool "ex" (Set (Var "p5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p5")) "," (Set (Var "p7")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "p5")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "e"))) ")" )) & (Bool "ex" (Set (Var "p6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p4")) "," (Set (Var "p6")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p6")) "," (Set (Var "p7")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "p6")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" )) ")" ) ")" ) ")" )) ")" ) ")" )))); :: deftheorem defines :::"is_OSout"::: JORDAN20:def 6 : (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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r6_jordan20 :::"is_OSout"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))) "iff" (Bool "(" (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool "ex" (Set (Var "p7")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p")) "," (Set (Var "p7")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool "(" "for" (Set (Var "p8")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p8")) "," (Set (Var "p7")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p")) "," (Set (Var "p8")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Set (Var "p8")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" ) & (Bool "(" "for" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p7")) "," (Set (Var "p4")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "p4")) ($#r1_hidden :::"<>"::: ) (Set (Var "p7")))) "holds" (Bool "(" (Bool "ex" (Set (Var "p5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p5")) "," (Set (Var "p4")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p7")) "," (Set (Var "p5")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "p5")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "e"))) ")" )) & (Bool "ex" (Set (Var "p6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p6")) "," (Set (Var "p4")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "p7")) "," (Set (Var "p6")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "p6")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" )) ")" ) ")" ) ")" )) ")" ) ")" )))); theorem :: JORDAN20:8 (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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "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 (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "e"))) & (Bool (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "e")))) "holds" (Bool "ex" (Set (Var "p3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "p3")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" ))))) ; theorem :: JORDAN20:9 (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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "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 (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_jordan20 :::"is_Lin"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e")))) & (Bool (Bool "not" (Set (Var "p")) ($#r2_jordan20 :::"is_Rin"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))))) "holds" (Bool (Set (Var "p")) ($#r5_jordan20 :::"is_OSin"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e")))))) ; theorem :: JORDAN20:10 (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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "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 (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "e"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Bool "not" (Set (Var "p")) ($#r3_jordan20 :::"is_Lout"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e")))) & (Bool (Bool "not" (Set (Var "p")) ($#r4_jordan20 :::"is_Rout"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))))) "holds" (Bool (Set (Var "p")) ($#r6_jordan20 :::"is_OSout"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e")))))) ; theorem :: JORDAN20:11 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "s")) ($#k3_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: JORDAN20:12 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "s")) "," (Num 1) ($#k4_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: JORDAN20:13 (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")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q0")) where q0 "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "ex" (Set (Var "ss")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "ss"))) & (Bool (Set (Var "ss")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "q0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "ss")))) ")" )) "}" ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "s")) ($#k3_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set (Var "P1")))))))) ; theorem :: JORDAN20:14 (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")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q0")) where q0 "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "ex" (Set (Var "ss")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ss"))) & (Bool (Set (Var "ss")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "q0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "ss")))) ")" )) "}" ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "s")) "," (Num 1) ($#k4_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set (Var "P1")))))))) ; theorem :: JORDAN20:15 (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")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) & (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q0")) where q0 "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "ex" (Set (Var "ss")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "ss"))) & (Bool (Set (Var "ss")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "q0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "ss")))) ")" )) "}" )) "holds" (Bool (Set (Var "P1")) "is" ($#v3_pre_topc :::"open"::: ) ))))) ; theorem :: JORDAN20:16 (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")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) & (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q0")) where q0 "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "ex" (Set (Var "ss")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ss"))) & (Bool (Set (Var "ss")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "q0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "ss")))) ")" )) "}" )) "holds" (Bool (Set (Var "P1")) "is" ($#v3_pre_topc :::"open"::: ) ))))) ; theorem :: JORDAN20:17 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Q1")) "," (Set (Var "Q2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "Q1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Q2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "Q1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Q2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) & (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "Q1"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q2"))) & (Bool (Set (Var "Q1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "Q2")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "T")) "holds" (Bool "(" "not" (Bool (Set (Var "P")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "or" "not" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) "or" "not" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) ")" ))))) ; theorem :: JORDAN20: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 "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")) "," (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")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "q")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "Q")) "is" ($#v2_connsp_1 :::"connected"::: ) )) & (Bool "(" "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "Q")) ")" ) "holds" (Bool "(" "not" (Bool (Set (Var "R")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "or" "not" (Bool (Set (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) "or" "not" (Bool (Set (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) ")" ) ")" ) ")" )))) ; theorem :: JORDAN20: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) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Bool "not" ($#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 "p1")) "," (Set (Var "p2"))))) ; theorem :: JORDAN20:20 (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 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "P1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "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 "P1")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set (Var "P")))))) ; theorem :: JORDAN20:21 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "q1")))) "holds" (Bool (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "p2")) ")" ) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "q1")) "," (Set (Var "p2"))))) ; theorem :: JORDAN20:22 (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")) "," (Set (Var "q3")) "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"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Set "(" ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q2")) "," (Set (Var "q3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q3")) ")" )))) ; theorem :: JORDAN20:23 (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")) "," (Set (Var "q3")) "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"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Set "(" ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q2")) "," (Set (Var "q3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "q2")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: JORDAN20:24 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "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 "p1")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "P"))))) ; theorem :: JORDAN20:25 (Bool "for" (Set (Var "P")) "," (Set (Var "Q1")) "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) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "Q1")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "q1")) "," (Set (Var "q2"))) & (Bool ($#r1_jordan5c :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "Q1")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "Q1")) ($#r1_hidden :::"="::: ) (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" )))) ; theorem :: JORDAN20:26 (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")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "q1")) ($#r1_jordan20 :::"is_Lin"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))) & (Bool (Set (Set (Var "q2")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ))) "holds" (Bool (Set (Var "p")) ($#r1_jordan20 :::"is_Lin"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e")))))) ; theorem :: JORDAN20:27 (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")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "q1")) ($#r2_jordan20 :::"is_Rin"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))) & (Bool (Set (Set (Var "q2")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ))) "holds" (Bool (Set (Var "p")) ($#r2_jordan20 :::"is_Rin"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e")))))) ; theorem :: JORDAN20:28 (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")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "q1")) ($#r3_jordan20 :::"is_Lout"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))) & (Bool (Set (Set (Var "q2")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ))) "holds" (Bool (Set (Var "p")) ($#r3_jordan20 :::"is_Lout"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e")))))) ; theorem :: JORDAN20:29 (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")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "q1")) ($#r4_jordan20 :::"is_Rout"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))) & (Bool (Set (Set (Var "q2")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ))) "holds" (Bool (Set (Var "p")) ($#r4_jordan20 :::"is_Rout"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e")))))) ; theorem :: JORDAN20:30 (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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_jordan20 :::"is_Lin"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))))) "holds" (Bool (Set (Var "p")) ($#r2_jordan20 :::"is_Rin"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e")))))) ; theorem :: JORDAN20:31 (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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "e"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Bool "not" (Set (Var "p")) ($#r3_jordan20 :::"is_Lout"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e"))))) "holds" (Bool (Set (Var "p")) ($#r4_jordan20 :::"is_Rout"::: ) (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "e")))))) ;