:: JORDAN21 semantic presentation begin theorem :: JORDAN21:1 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; theorem :: JORDAN21:2 (Bool "for" (Set (Var "s1")) "," (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s "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 :: JORDAN21:3 (Bool "for" (Set (Var "s2")) "," (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where s "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 :: JORDAN21:4 (Bool "for" (Set (Var "s")) "," (Set (Var "t1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where 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 :: JORDAN21:5 (Bool "for" (Set (Var "s")) "," (Set (Var "t2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k19_euclid :::"]|"::: ) ) where 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 :: JORDAN21:6 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k4_topreal1 :::"north_halfline"::: ) (Set (Var "p")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v1_convex1 :::"convex"::: ) )) ; theorem :: JORDAN21:7 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k6_topreal1 :::"south_halfline"::: ) (Set (Var "p")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v1_convex1 :::"convex"::: ) )) ; theorem :: JORDAN21:8 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k7_topreal1 :::"west_halfline"::: ) (Set (Var "p")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v1_convex1 :::"convex"::: ) )) ; theorem :: JORDAN21:9 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k5_topreal1 :::"east_halfline"::: ) (Set (Var "p")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v1_convex1 :::"convex"::: ) )) ; theorem :: JORDAN21:10 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "holds" (Bool (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "A"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A")))) ; theorem :: JORDAN21:11 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "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 "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q1"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" ))) & (Bool (Bool "not" (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set (Var "P")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) ")" ))) ")" ))) ; definitionlet "D" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); attr "D" is :::"with_the_max_arc"::: means :: JORDAN21:def 1 (Bool "D" ($#r1_xboole_0 :::"meets"::: ) (Set ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) "D" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) "D" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ))); end; :: deftheorem defines :::"with_the_max_arc"::: JORDAN21:def 1 : (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v1_jordan21 :::"with_the_max_arc"::: ) ) "iff" (Bool (Set (Var "D")) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "D")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "D")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ))) ")" )); registration cluster ($#v1_jordan21 :::"with_the_max_arc"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )))); end; registration cluster ($#v1_topreal2 :::"being_simple_closed_curve"::: ) -> ($#v1_jordan21 :::"with_the_max_arc"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )))); end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_pre_topc :::"closed"::: ) ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#v9_rltopsp1 :::"bounded"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#v1_topreal2 :::"being_simple_closed_curve"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )))); end; theorem :: JORDAN21:12 (Bool "for" (Set (Var "D")) "being" ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Bool "not" (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "D")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "D")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "D")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) ))) ; theorem :: JORDAN21:13 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )) "is" ($#v2_rcomp_1 :::"closed"::: ) ) & (Bool (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ")" )) ; begin theorem :: JORDAN21:14 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k10_jordan6 :::"Lower_Middle_Point"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) ; theorem :: JORDAN21:15 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set (Set "(" ($#k10_jordan6 :::"Lower_Middle_Point"::: ) (Set (Var "C")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k11_jordan6 :::"Upper_Middle_Point"::: ) (Set (Var "C")) ")" ) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: JORDAN21:16 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k10_jordan6 :::"Lower_Middle_Point"::: ) (Set (Var "C"))) ($#r1_hidden :::"<>"::: ) (Set ($#k11_jordan6 :::"Upper_Middle_Point"::: ) (Set (Var "C"))))) ; begin theorem :: JORDAN21:17 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")) ")" )))) ; theorem :: JORDAN21:18 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")) ")" )))) ; theorem :: JORDAN21:19 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" )))) ; theorem :: JORDAN21:20 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" )))) ; theorem :: JORDAN21:21 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool "(" (Bool (Bool "not" (Set (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; theorem :: JORDAN21:22 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool "(" (Bool (Bool "not" (Set (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )) ; theorem :: JORDAN21:23 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "P")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Bool "not" (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "P"))))) "holds" (Bool (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "P"))))) ; registrationlet "C" be ($#m1_subset_1 :::"Simple_closed_curve":::); cluster (Set ($#k9_jordan6 :::"Lower_Arc"::: ) "C") -> ($#v1_jordan21 :::"with_the_max_arc"::: ) ; cluster (Set ($#k8_jordan6 :::"Upper_Arc"::: ) "C") -> ($#v1_jordan21 :::"with_the_max_arc"::: ) ; end; begin definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); func :::"UMP"::: "P" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN21:def 2 (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) "P" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) "P" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" "P" ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) "P" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) "P" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ); func :::"LMP"::: "P" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN21:def 3 (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) "P" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) "P" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" "P" ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) "P" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) "P" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ); end; :: deftheorem defines :::"UMP"::: JORDAN21:def 2 : (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "holds" (Bool (Set ($#k1_jordan21 :::"UMP"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "P")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))); :: deftheorem defines :::"LMP"::: JORDAN21:def 3 : (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "holds" (Bool (Set ($#k2_jordan21 :::"LMP"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "P")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))); theorem :: JORDAN21:24 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C"))) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C"))))) ; theorem :: JORDAN21:25 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C"))) ($#r1_hidden :::"<>"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))))) ; theorem :: JORDAN21:26 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C"))) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C"))))) ; theorem :: JORDAN21:27 (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C"))) ($#r1_hidden :::"<>"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))))) ; theorem :: JORDAN21:28 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )))) "holds" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C")) ")" ) ($#k18_euclid :::"`2"::: ) )))) ; theorem :: JORDAN21:29 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "C")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )))) "holds" (Bool (Set (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) )))) ; theorem :: JORDAN21:30 (Bool "for" (Set (Var "D")) "being" ($#v2_compts_1 :::"compact"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_jordan21 :::"UMP"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) ; theorem :: JORDAN21:31 (Bool "for" (Set (Var "D")) "being" ($#v2_compts_1 :::"compact"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k2_jordan21 :::"LMP"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) ; theorem :: JORDAN21:32 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "P")) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "P")) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) )) ; theorem :: JORDAN21:33 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "P")) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "P")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "P")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "P")) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) )) ; theorem :: JORDAN21:34 (Bool "for" (Set (Var "D")) "being" ($#v2_compts_1 :::"compact"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "D")) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "D")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "D")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "D")) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "D")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ; theorem :: JORDAN21:35 (Bool "for" (Set (Var "D")) "being" ($#v2_compts_1 :::"compact"::: ) ($#v1_jordan21 :::"with_the_max_arc"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "D")) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "D")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "D")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "D")) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "D")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ; theorem :: JORDAN21:36 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C")) ")" ) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: JORDAN21:37 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C"))))) ; theorem :: JORDAN21:38 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C")) ")" ) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: JORDAN21:39 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C"))))) ; theorem :: JORDAN21:40 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C")) ")" ) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: JORDAN21:41 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C"))))) ; theorem :: JORDAN21:42 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C")) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C")) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C")) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C")) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ))) ; theorem :: JORDAN21:43 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "B")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "B")) ")" ))) & (Bool (Bool "not" (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "A")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "A")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool (Set (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "A")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set (Var "B")) ")" ) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: JORDAN21:44 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "B")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "B")) ")" ))) & (Bool (Bool "not" (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "A")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "A")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool (Set (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "B")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set (Var "A")) ")" ) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: JORDAN21:45 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set ($#k1_jordan21 :::"UMP"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Bool "not" (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "A")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "B")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "B")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool (Set (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "B")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "B")) ")" )))) "holds" (Bool (Set ($#k1_jordan21 :::"UMP"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan21 :::"UMP"::: ) (Set (Var "B"))))) ; theorem :: JORDAN21:46 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set ($#k2_jordan21 :::"LMP"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Bool "not" (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "A")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_jordan6 :::"Vertical_Line"::: ) (Set "(" (Set "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "B")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "B")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "B")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "B")) ")" )))) "holds" (Bool (Set ($#k2_jordan21 :::"LMP"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_jordan21 :::"LMP"::: ) (Set (Var "B"))))) ; theorem :: JORDAN21:47 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set (Set "(" ($#k1_jordan21 :::"UMP"::: ) (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C"))))) ; theorem :: JORDAN21:48 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k2_jordan21 :::"LMP"::: ) (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: JORDAN21:49 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool "(" "not" (Bool (Set ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")))) "or" "not" (Bool (Set ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")))) ")" )) ; theorem :: JORDAN21:50 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool "(" "not" (Bool (Set ($#k2_jordan21 :::"LMP"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")))) "or" "not" (Bool (Set ($#k1_jordan21 :::"UMP"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")))) ")" )) ;