:: JORDAN1 semantic presentation begin theorem :: JORDAN1:1 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX")) (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set (Var "GX")) "st" (Bool "(" (Bool (Set (Var "h")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Num 1))) ")" )) ")" )) "holds" (Bool (Set (Var "GX")) "is" ($#v1_connsp_1 :::"connected"::: ) )) ; theorem :: JORDAN1:2 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool "(" "for" (Set (Var "xa")) "," (Set (Var "ya")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "xa")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "ya")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "xa")) ($#r1_hidden :::"<>"::: ) (Set (Var "ya")))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set "(" (Set (Var "GX")) ($#k1_pre_topc :::"|"::: ) (Set (Var "A")) ")" ) "st" (Bool "(" (Bool (Set (Var "h")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "xa")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "ya")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Num 1))) ")" )) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) ))) ; theorem :: JORDAN1:3 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A0")) "," (Set (Var "A1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A0")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A1")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A0")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A1")))) "holds" (Bool (Set (Set (Var "A0")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A1"))) "is" ($#v2_connsp_1 :::"connected"::: ) ))) ; theorem :: JORDAN1:4 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A0")) "," (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A0")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A1")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A0")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A1"))) & (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A2")))) "holds" (Bool (Set (Set "(" (Set (Var "A0")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) "is" ($#v2_connsp_1 :::"connected"::: ) ))) ; theorem :: JORDAN1:5 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A0")) "," (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A0")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A1")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A3")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A0")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A1"))) & (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A2")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A3")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "A0")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A3"))) "is" ($#v2_connsp_1 :::"connected"::: ) ))) ; begin definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); redefine attr "P" is :::"convex"::: means :: JORDAN1:def 1 (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" "st" (Bool (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_tarski :::"c="::: ) "P")); end; :: deftheorem defines :::"convex"::: JORDAN1:def 1 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v1_convex1 :::"convex"::: ) ) "iff" (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) ")" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#v1_convex1 :::"convex"::: ) -> ($#v2_connsp_1 :::"connected"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" )))); end; theorem :: JORDAN1:6 canceled; theorem :: JORDAN1:7 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t"))) & (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s3")) "," (Set (Var "t3")) ($#k19_euclid :::"]|"::: ) ) where s3, t3 "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s3"))) "}" ($#k3_xboole_0 :::"/\"::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s4")) "," (Set (Var "t4")) ($#k19_euclid :::"]|"::: ) ) where s4, t4 "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s4")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) "}" ")" ) ($#k3_xboole_0 :::"/\"::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s5")) "," (Set (Var "t5")) ($#k19_euclid :::"]|"::: ) ) where s5, t5 "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t5"))) "}" ")" ) ($#k3_xboole_0 :::"/\"::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s6")) "," (Set (Var "t6")) ($#k19_euclid :::"]|"::: ) ) where s6, t6 "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "t6")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) "}" ))) ; theorem :: JORDAN1:8 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) "or" "not" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t"))) "or" "not" (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s3")) "," (Set (Var "t3")) ($#k19_euclid :::"]|"::: ) ) where s3, t3 "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s3")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s1"))) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s4")) "," (Set (Var "t4")) ($#k19_euclid :::"]|"::: ) ) where s4, t4 "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "t4")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t1"))) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s5")) "," (Set (Var "t5")) ($#k19_euclid :::"]|"::: ) ) where s5, t5 "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s2")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s5"))) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s6")) "," (Set (Var "t6")) ($#k19_euclid :::"]|"::: ) ) where s6, t6 "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "t2")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t6"))) "}" ))) ; theorem :: JORDAN1:9 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t"))) & (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v1_convex1 :::"convex"::: ) ))) ; theorem :: JORDAN1:10 canceled; theorem :: JORDAN1:11 (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v1_convex1 :::"convex"::: ) ))) ; theorem :: JORDAN1:12 canceled; theorem :: JORDAN1:13 (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v1_convex1 :::"convex"::: ) ))) ; theorem :: JORDAN1:14 canceled; theorem :: JORDAN1:15 (Bool "for" (Set (Var "t1")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v1_convex1 :::"convex"::: ) ))) ; theorem :: JORDAN1:16 canceled; theorem :: JORDAN1:17 (Bool "for" (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v1_convex1 :::"convex"::: ) ))) ; theorem :: JORDAN1:18 canceled; theorem :: JORDAN1:19 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) "or" "not" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t"))) "or" "not" (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v2_connsp_1 :::"connected"::: ) ))) ; theorem :: JORDAN1:20 (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: JORDAN1:21 (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "s"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: JORDAN1:22 (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: JORDAN1:23 (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "t"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: JORDAN1:24 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t"))) & (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: JORDAN1:25 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s, t "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) "or" "not" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t"))) "or" "not" (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: JORDAN1:26 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "sa")) "," (Set (Var "ta")) ($#k19_euclid :::"]|"::: ) ) where sa, ta "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "sa"))) & (Bool (Set (Var "sa")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ta"))) & (Bool (Set (Var "ta")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "sb")) "," (Set (Var "tb")) ($#k19_euclid :::"]|"::: ) ) where sb, tb "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "sb"))) "or" "not" (Bool (Set (Var "sb")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "tb"))) "or" "not" (Bool (Set (Var "tb")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Q"))))) ; theorem :: JORDAN1:27 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "sa")) "," (Set (Var "ta")) ($#k19_euclid :::"]|"::: ) ) where sa, ta "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "sa"))) & (Bool (Set (Var "sa")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ta"))) & (Bool (Set (Var "ta")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" )) ; theorem :: JORDAN1:28 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "{" (Set (Var "qc")) where qc "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "qc")) ($#k17_euclid :::"`1"::: ) )) "or" "not" (Bool (Set (Set (Var "qc")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "qc")) ($#k18_euclid :::"`2"::: ) )) "or" "not" (Bool (Set (Set (Var "qc")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "sb")) "," (Set (Var "tb")) ($#k19_euclid :::"]|"::: ) ) where sb, tb "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "sb"))) "or" "not" (Bool (Set (Var "sb")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "tb"))) "or" "not" (Bool (Set (Var "tb")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" )) ; theorem :: JORDAN1:29 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "{" (Set (Var "p0")) where p0 "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p0")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p0")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p0")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "p0")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))) ; theorem :: JORDAN1:30 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "{" (Set (Var "pq")) where pq "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pq")) ($#k17_euclid :::"`1"::: ) )) "or" "not" (Bool (Set (Set (Var "pq")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pq")) ($#k18_euclid :::"`2"::: ) )) "or" "not" (Bool (Set (Set (Var "pq")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))) ; theorem :: JORDAN1:31 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (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 "p0")) where p0 "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p0")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p0")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p0")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "p0")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v1_convex1 :::"convex"::: ) ))) ; theorem :: JORDAN1:32 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (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 "pq")) where pq "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pq")) ($#k17_euclid :::"`1"::: ) )) "or" "not" (Bool (Set (Set (Var "pq")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pq")) ($#k18_euclid :::"`2"::: ) )) "or" "not" (Bool (Set (Set (Var "pq")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v2_connsp_1 :::"connected"::: ) ))) ; theorem :: JORDAN1:33 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (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 "p0")) where p0 "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p0")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p0")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p0")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "p0")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: JORDAN1:34 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (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 "pq")) where pq "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pq")) ($#k17_euclid :::"`1"::: ) )) "or" "not" (Bool (Set (Set (Var "pq")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pq")) ($#k18_euclid :::"`2"::: ) )) "or" "not" (Bool (Set (Set (Var "pq")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: JORDAN1:35 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "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 "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) "{" (Set (Var "qc")) where qc "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "qc")) ($#k17_euclid :::"`1"::: ) )) "or" "not" (Bool (Set (Set (Var "qc")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "qc")) ($#k18_euclid :::"`2"::: ) )) "or" "not" (Bool (Set (Set (Var "qc")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Q"))))) ; theorem :: JORDAN1:36 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "," (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) & (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 "(" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t2"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) ")" ) "}" ) & (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "pa")) where pa "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "pa")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "pa")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "pa")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "pa")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" ) & (Bool (Set (Var "P2")) ($#r1_hidden :::"="::: ) "{" (Set (Var "pb")) where pb "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pb")) ($#k17_euclid :::"`1"::: ) )) "or" "not" (Bool (Set (Set (Var "pb")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pb")) ($#k18_euclid :::"`2"::: ) )) "or" "not" (Bool (Set (Set (Var "pb")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool "(" (Bool (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "P2")))) & (Bool (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "P2"))) & (Bool "(" "for" (Set (Var "P1A")) "," (Set (Var "P2B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) "st" (Bool (Bool (Set (Var "P1A")) ($#r1_hidden :::"="::: ) (Set (Var "P1"))) & (Bool (Set (Var "P2B")) ($#r1_hidden :::"="::: ) (Set (Var "P2")))) "holds" (Bool "(" (Bool (Set (Var "P1A")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "P2B")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) ")" ) ")" ) ")" ))) ; theorem :: JORDAN1:37 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "," (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) & (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 "(" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t2"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) ")" ) "}" ) & (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "pa")) where pa "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "pa")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "pa")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "pa")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "pa")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" ) & (Bool (Set (Var "P2")) ($#r1_hidden :::"="::: ) "{" (Set (Var "pb")) where pb "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pb")) ($#k17_euclid :::"`1"::: ) )) "or" "not" (Bool (Set (Set (Var "pb")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pb")) ($#k18_euclid :::"`2"::: ) )) "or" "not" (Bool (Set (Set (Var "pb")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "P1")))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P2")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "P2")))) ")" ))) ; theorem :: JORDAN1:38 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "," (Set (Var "P1")) "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 "(" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t2"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) ")" ) "}" ) & (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "pa")) where pa "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "pa")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "pa")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "pa")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "pa")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ))))) ; theorem :: JORDAN1:39 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "," (Set (Var "P1")) "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 "(" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t2"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) ")" ) "}" ) & (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "pa")) where pa "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "pa")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "pa")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "pa")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "pa")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P1")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" )))) ; theorem :: JORDAN1:40 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) & (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 "(" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t2"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) ")" ) "}" ) & (Bool (Set (Var "P2")) ($#r1_hidden :::"="::: ) "{" (Set (Var "pb")) where pb "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pb")) ($#k17_euclid :::"`1"::: ) )) "or" "not" (Bool (Set (Set (Var "pb")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pb")) ($#k18_euclid :::"`2"::: ) )) "or" "not" (Bool (Set (Set (Var "pb")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P2")) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ))))) ; theorem :: JORDAN1:41 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) & (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 "(" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t2"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) ")" ) "}" ) & (Bool (Set (Var "P2")) ($#r1_hidden :::"="::: ) "{" (Set (Var "pb")) where pb "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pb")) ($#k17_euclid :::"`1"::: ) )) "or" "not" (Bool (Set (Set (Var "pb")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pb")) ($#k18_euclid :::"`2"::: ) )) "or" "not" (Bool (Set (Set (Var "pb")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set (Var "P2")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" )))) ; begin definitionlet "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); attr "S" is :::"Jordan"::: means :: JORDAN1:def 2 (Bool "(" (Bool (Set "S" ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set "S" ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A2")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A2")))) & (Bool "(" "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" "S" ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) "st" (Bool (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "A1"))) & (Bool (Set (Var "C2")) ($#r1_hidden :::"="::: ) (Set (Var "A2")))) "holds" (Bool "(" (Bool (Set (Var "C1")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) ")" ) ")" ) ")" )) ")" ); end; :: deftheorem defines :::"Jordan"::: JORDAN1:def 2 : (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_jordan1 :::"Jordan"::: ) ) "iff" (Bool "(" (Bool (Set (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A2")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A2")))) & (Bool "(" "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) "st" (Bool (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "A1"))) & (Bool (Set (Var "C2")) ($#r1_hidden :::"="::: ) (Set (Var "A2")))) "holds" (Bool "(" (Bool (Set (Var "C1")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) ")" ) ")" ) ")" )) ")" ) ")" )); theorem :: JORDAN1:42 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "S")) "is" ($#v1_jordan1 :::"Jordan"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )(Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A2")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A2")))) & (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "A1"))) & (Bool (Set (Var "C2")) ($#r1_hidden :::"="::: ) (Set (Var "A2"))) & (Bool (Set (Var "C1")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool "(" "for" (Set (Var "C3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) "holds" (Bool "(" "not" (Bool (Set (Var "C3")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) "or" (Bool (Set (Var "C3")) ($#r1_hidden :::"="::: ) (Set (Var "C1"))) "or" (Bool (Set (Var "C3")) ($#r1_hidden :::"="::: ) (Set (Var "C2"))) ")" ) ")" ) ")" ))) ")" )) ; theorem :: JORDAN1:43 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) & (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 "(" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t2"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v1_jordan1 :::"Jordan"::: ) ))) ; theorem :: JORDAN1:44 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) & (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 "(" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t2"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) ")" ) "}" ) & (Bool (Set (Var "P2")) ($#r1_hidden :::"="::: ) "{" (Set (Var "pb")) where pb "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" "not" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pb")) ($#k17_euclid :::"`1"::: ) )) "or" "not" (Bool (Set (Set (Var "pb")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) "or" "not" (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pb")) ($#k18_euclid :::"`2"::: ) )) "or" "not" (Bool (Set (Set (Var "pb")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "P2")))))) ; theorem :: JORDAN1:45 (Bool "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "," (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) & (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 "(" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t2"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t1"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t1"))) ")" ) ")" ) "}" ) & (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "pa")) where pa "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "pa")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "pa")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2"))) & (Bool (Set (Var "t1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "pa")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "pa")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t2"))) ")" ) "}" )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "P1")))))) ; theorem :: JORDAN1:46 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_tarski :::"}"::: ) )) "is" ($#v1_convex1 :::"convex"::: ) )) ; registrationlet "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k4_topreal1 :::"north_halfline"::: ) "p") -> ($#v1_convex1 :::"convex"::: ) ; cluster (Set ($#k5_topreal1 :::"east_halfline"::: ) "p") -> ($#v1_convex1 :::"convex"::: ) ; cluster (Set ($#k6_topreal1 :::"south_halfline"::: ) "p") -> ($#v1_convex1 :::"convex"::: ) ; cluster (Set ($#k7_topreal1 :::"west_halfline"::: ) "p") -> ($#v1_convex1 :::"convex"::: ) ; end;