:: JORDAN18  semantic presentation begin  





























theorem :: JORDAN18:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: JORDAN18:2 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Var "A")) "is"   ($#v2_compts_1 :::"compact"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set (Var "A"))) "is"   ($#v2_compts_1 :::"compact"::: )  )))) ; 
 
theorem :: JORDAN18:3 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k4_topreal1 :::"north_halfline"::: )  (Set (Var "a")) ")" )) "is"   ($#v3_xxreal_2 :::"bounded_below"::: )  )) ; 
 
theorem :: JORDAN18:4 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k6_topreal1 :::"south_halfline"::: )  (Set (Var "a")) ")" )) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  )) ; 
 
theorem :: JORDAN18:5 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k7_topreal1 :::"west_halfline"::: )  (Set (Var "a")) ")" )) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  )) ; 
 
theorem :: JORDAN18:6 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k5_topreal1 :::"east_halfline"::: )  (Set (Var "a")) ")" )) "is"   ($#v3_xxreal_2 :::"bounded_below"::: )  )) ; 
 registrationlet "a" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); 
cluster (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relat_1 :::".:"::: )  (Set  "("  ($#k4_topreal1 :::"north_halfline"::: )  "a" ")" )) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relat_1 :::".:"::: )  (Set  "("  ($#k6_topreal1 :::"south_halfline"::: )  "a" ")" )) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k7_relat_1 :::".:"::: )  (Set  "("  ($#k7_topreal1 :::"west_halfline"::: )  "a" ")" )) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k7_relat_1 :::".:"::: )  (Set  "("  ($#k5_topreal1 :::"east_halfline"::: )  "a" ")" )) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: JORDAN18:7 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k4_topreal1 :::"north_halfline"::: )  (Set (Var "a")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k18_euclid :::"`2"::: )  ))) ; 
 
theorem :: JORDAN18:8 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k6_topreal1 :::"south_halfline"::: )  (Set (Var "a")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k18_euclid :::"`2"::: )  ))) ; 
 
theorem :: JORDAN18:9 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k7_topreal1 :::"west_halfline"::: )  (Set (Var "a")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k17_euclid :::"`1"::: )  ))) ; 
 
theorem :: JORDAN18:10 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k5_topreal1 :::"east_halfline"::: )  (Set (Var "a")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k17_euclid :::"`1"::: )  ))) ; 
 registrationlet "a" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); 
cluster (Set   ($#k4_topreal1 :::"north_halfline"::: )  "a") ->   ($#v4_pre_topc :::"closed"::: )   ; 

cluster (Set   ($#k6_topreal1 :::"south_halfline"::: )  "a") ->   ($#v4_pre_topc :::"closed"::: )   ; 

cluster (Set   ($#k5_topreal1 :::"east_halfline"::: )  "a") ->   ($#v4_pre_topc :::"closed"::: )   ; 

cluster (Set   ($#k7_topreal1 :::"west_halfline"::: )  "a") ->   ($#v4_pre_topc :::"closed"::: )   ; 
end; 
theorem :: JORDAN18:11 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "P"))))) "holds"  (Bool  "not" (Bool (Set   ($#k4_topreal1 :::"north_halfline"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_jordan2c :::"UBD"::: )  (Set (Var "P"))))))) ; 
 
theorem :: JORDAN18:12 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "P"))))) "holds"  (Bool  "not" (Bool (Set   ($#k6_topreal1 :::"south_halfline"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_jordan2c :::"UBD"::: )  (Set (Var "P"))))))) ; 
 
theorem :: JORDAN18:13 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "P"))))) "holds"  (Bool  "not" (Bool (Set   ($#k5_topreal1 :::"east_halfline"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_jordan2c :::"UBD"::: )  (Set (Var "P"))))))) ; 
 
theorem :: JORDAN18:14 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "P"))))) "holds"  (Bool  "not" (Bool (Set   ($#k7_topreal1 :::"west_halfline"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_jordan2c :::"UBD"::: )  (Set (Var "P"))))))) ; 
 
theorem :: JORDAN18:15 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P"))  ($#r1_tarski :::"c="::: )  (Set (Var "C")))) "holds"  (Bool  "ex" (Set (Var "R")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "R"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "P"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set (Var "C"))) & (Bool (Set (Set (Var "P"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) ))  ")" ))))) ; 
 begin  definitionlet "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); let "P" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); func  :::"North-Bound":::  "(" "p" "," "P" ")"  ->   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) equals :: JORDAN18:def 1 (Set  ($#k19_euclid :::"|["::: ) (Set  "(" "p"  ($#k17_euclid :::"`1"::: )  ")" ) "," (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "(" "P"  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_topreal1 :::"north_halfline"::: )  "p" ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ); func  :::"South-Bound":::  "(" "p" "," "P" ")"  ->   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) equals :: JORDAN18:def 2 (Set  ($#k19_euclid :::"|["::: ) (Set  "(" "p"  ($#k17_euclid :::"`1"::: )  ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "(" "P"  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k6_topreal1 :::"south_halfline"::: )  "p" ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ); end; 












:: deftheorem    defines :::"North-Bound"::: JORDAN18:def 1 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k1_jordan18 :::"North-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "P")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) "," (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "(" (Set (Var "P"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_topreal1 :::"north_halfline"::: )  (Set (Var "p")) ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) )))); 
 
:: deftheorem    defines :::"South-Bound"::: JORDAN18:def 2 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k2_jordan18 :::"South-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "P")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "(" (Set (Var "P"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k6_topreal1 :::"south_halfline"::: )  (Set (Var "p")) ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) )))); 
 
theorem :: JORDAN18:16 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k1_jordan18 :::"North-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "P")) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "("  ($#k2_jordan18 :::"South-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "P")) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ))  ")" ))) ; 
 
theorem :: JORDAN18:17 (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   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C"))))) "holds"  (Bool  "("  (Bool (Set   ($#k1_jordan18 :::"North-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set   ($#k1_jordan18 :::"North-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k4_topreal1 :::"north_halfline"::: )  (Set (Var "p")))) & (Bool (Set   ($#k2_jordan18 :::"South-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set   ($#k2_jordan18 :::"South-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k6_topreal1 :::"south_halfline"::: )  (Set (Var "p"))))  ")" ))) ; 
 
theorem :: JORDAN18:18 (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   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C"))))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k2_jordan18 :::"South-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k1_jordan18 :::"North-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" ))) ; 
 
theorem :: JORDAN18:19 (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   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C"))))) "holds"  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "(" (Set (Var "C"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_topreal1 :::"north_halfline"::: )  (Set (Var "p")) ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "(" (Set (Var "C"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k6_topreal1 :::"south_halfline"::: )  (Set (Var "p")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: JORDAN18:20 (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   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C"))))) "holds"  (Bool (Set   ($#k2_jordan18 :::"South-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_jordan18 :::"North-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")" )))) ; 
 
theorem :: JORDAN18:21 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "("  ($#k1_jordan18 :::"North-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")"  ")" ) "," (Set  "("  ($#k2_jordan18 :::"South-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")"  ")" ) ")" ) "is"   ($#v2_sppol_1 :::"vertical"::: )  ))) ; 
 
theorem :: JORDAN18:22 (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   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Set  "("  ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "("  ($#k1_jordan18 :::"North-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")"  ")" ) "," (Set  "("  ($#k2_jordan18 :::"South-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")"  ")" ) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  "("  ($#k1_jordan18 :::"North-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")"  ")" ) "," (Set  "("  ($#k2_jordan18 :::"South-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")"  ")" ) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: JORDAN18:23 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "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   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C")))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_jordan2c :::"BDD"::: )  (Set (Var "C")))) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  ))) "holds"  (Bool (Set   ($#k1_jordan18 :::"North-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")" ) "," (Set   ($#k2_jordan18 :::"South-Bound"::: )   "(" (Set (Var "q")) "," (Set (Var "C")) ")" ) "," (Set   ($#k1_jordan18 :::"North-Bound"::: )   "(" (Set (Var "q")) "," (Set (Var "C")) ")" ) "," (Set   ($#k2_jordan18 :::"South-Bound"::: )   "(" (Set (Var "p")) "," (Set (Var "C")) ")" )  ($#r2_zfmisc_1 :::"are_mutually_different"::: )  ))) ; 
 begin  definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "V" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "s1", "s2", "t1", "t2" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); pred "s1" "," "s2" "," "V" :::"-separate"::: "t1" "," "t2" means :: JORDAN18:def 3 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  "s1" "," "s2") & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  "V")) "holds"  (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"meets"::: )  (Set  ($#k2_tarski :::"{"::: ) "t1" "," "t2" ($#k2_tarski :::"}"::: ) ))); end; 









:: deftheorem    defines :::"-separate"::: JORDAN18:def 3 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "V"))  ($#r1_jordan18 :::"-separate"::: )  (Set (Var "t1")) "," (Set (Var "t2"))) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "s1")) "," (Set (Var "s2"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "V")))) "holds"  (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"meets"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "t1")) "," (Set (Var "t2")) ($#k2_tarski :::"}"::: ) )))  ")" )))); 
 notationlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "V" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "s1", "s2", "t1", "t2" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); antonym "s1" "," "s2" :::"are_neighbours_wrt"::: "t1" "," "t2" "," "V" for "s1" "," "s2" "," "V" :::"-separate"::: "t1" "," "t2"; end; 
theorem :: JORDAN18:24 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "t")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Var "t")) "," (Set (Var "t")) "," (Set (Var "V"))  ($#r1_jordan18 :::"-separate"::: )  (Set (Var "s1")) "," (Set (Var "s2")))))) ; 
 
theorem :: JORDAN18:25 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "V"))  ($#r1_jordan18 :::"-separate"::: )  (Set (Var "t1")) "," (Set (Var "t2")))) "holds"  (Bool (Set (Var "s2")) "," (Set (Var "s1")) "," (Set (Var "V"))  ($#r1_jordan18 :::"-separate"::: )  (Set (Var "t1")) "," (Set (Var "t2")))))) ; 
 
theorem :: JORDAN18:26 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "V"))  ($#r1_jordan18 :::"-separate"::: )  (Set (Var "t1")) "," (Set (Var "t2")))) "holds"  (Bool (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "V"))  ($#r1_jordan18 :::"-separate"::: )  (Set (Var "t2")) "," (Set (Var "t1")))))) ; 
 
theorem :: JORDAN18:27 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "s")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Var "s")) "," (Set (Var "t1")) "," (Set (Var "V"))  ($#r1_jordan18 :::"-separate"::: )  (Set (Var "s")) "," (Set (Var "t2")))))) ; 
 
theorem :: JORDAN18:28 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "t1")) "," (Set (Var "s")) "," (Set (Var "t2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Var "t1")) "," (Set (Var "s")) "," (Set (Var "V"))  ($#r1_jordan18 :::"-separate"::: )  (Set (Var "t2")) "," (Set (Var "s")))))) ; 
 
theorem :: JORDAN18:29 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "t1")) "," (Set (Var "s")) "," (Set (Var "t2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Var "t1")) "," (Set (Var "s")) "," (Set (Var "V"))  ($#r1_jordan18 :::"-separate"::: )  (Set (Var "s")) "," (Set (Var "t2")))))) ; 
 
theorem :: JORDAN18:30 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "s")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Var "s")) "," (Set (Var "t1")) "," (Set (Var "V"))  ($#r1_jordan18 :::"-separate"::: )  (Set (Var "t2")) "," (Set (Var "s")))))) ; 
 
theorem :: JORDAN18:31 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q")))) "holds"  (Bool (Set (Var "p1")) "," (Set (Var "p2"))  ($#r1_jordan18 :::"are_neighbours_wrt"::: )  (Set (Var "q")) "," (Set (Var "q")) "," (Set (Var "C"))))) ; 
 
theorem :: JORDAN18:32 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (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 "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "C"))  ($#r1_jordan18 :::"-separate"::: )  (Set (Var "q1")) "," (Set (Var "q2")))) "holds"  (Bool (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "C"))  ($#r1_jordan18 :::"-separate"::: )  (Set (Var "p1")) "," (Set (Var "p2"))))) ; 
 
theorem :: JORDAN18:33 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Simple_closed_curve":::)  (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 "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "q1"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p1"))) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p1"))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Bool  "not" (Set (Var "p1")) "," (Set (Var "p2"))  ($#r1_jordan18 :::"are_neighbours_wrt"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "C"))))) "holds"  (Bool (Set (Var "p1")) "," (Set (Var "q1"))  ($#r1_jordan18 :::"are_neighbours_wrt"::: )  (Set (Var "p2")) "," (Set (Var "q2")) "," (Set (Var "C"))))) ;