:: JGRAPH_5  semantic presentation begin  
theorem :: JGRAPH_5:1 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" )) ; 
 
theorem :: JGRAPH_5:2 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Num 1))  ")" )) ; 
 
theorem :: JGRAPH_5:3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "r3")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "PM")) "," (Set (Var "PM2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PM"))  (Bool  "for" (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PM2"))  "st" (Bool (Bool (Set (Var "d"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "e"))) & (Bool (Set (Var "PM"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "PM2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "d")) "," (Set (Var "e")) ")" )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x2")))) "holds"  (Bool (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "x")) "," (Set (Var "r3")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "x2")) "," (Set (Var "r3")) ")" )))))) ; 
 
theorem :: JGRAPH_5:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k5_topmetr :::"I[01]"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B")))))) ; 
 
theorem :: JGRAPH_5:5 (Bool  "for" (Set (Var "X")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "Y")) "," (Set (Var "Z")) "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 "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f"))) "is"   ($#v5_pre_topc :::"continuous"::: )  ))))) ; 
 
theorem :: JGRAPH_5:6 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )))) ; 
 
theorem :: JGRAPH_5:7 (Bool  "for" (Set (Var "X")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "S")) "," (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "(" (Set (Var "S"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "B")) ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "V"))  "st" (Bool (Bool (Set (Var "h"))  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool (Set (Var "h")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))))))) ; 
 
theorem :: JGRAPH_5:8 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "d")) "," (Set (Var "e")) ")"  ")" )  "st" (Bool (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set (Var "t1"))) & (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s2")))  ($#r1_hidden :::"="::: )  (Set (Var "t2"))) & (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "e"))) & (Bool (Set (Var "d"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "e"))) & (Bool (Set (Var "t1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "t2"))) & (Bool (Set (Var "s1"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "s2"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set (Var "s1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s2"))))) ; 
 
theorem :: JGRAPH_5:9 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "d")) "," (Set (Var "e")) ")"  ")" )  "st" (Bool (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set (Var "t1"))) & (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s2")))  ($#r1_hidden :::"="::: )  (Set (Var "t2"))) & (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) & (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "d"))) & (Bool (Set (Var "t1"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "t2"))) & (Bool (Set (Var "s1"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "s2"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set (Var "s1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s2"))))) ; 
 
theorem :: JGRAPH_5:10 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )))) ; 
 begin  
theorem :: JGRAPH_5:11 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "O")) "," (Set (Var "I")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )  "st" (Bool (Bool (Set (Var "O"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "I"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")) ")" )  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "d"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")) ")" )  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "d"))) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")) ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "d"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")) ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k17_euclid :::"`1"::: )  )) "or" (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Var "b"))) "or" (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k18_euclid :::"`2"::: )  )) "or" (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Var "d")))  ")" ) & (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k17_euclid :::"`1"::: )  )) "or" (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Var "b"))) "or" (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k18_euclid :::"`2"::: )  )) "or" (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Var "d")))  ")" )  ")" )  ")" )) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g"))))))) ; 
 
theorem :: JGRAPH_5:12 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool  "ex" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))) & (Bool (Set (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f2")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))) & (Bool (Set (Var "f2")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )  ")" ))) ; 
 




theorem :: JGRAPH_5:13 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "C0")) "," (Set (Var "KXP")) "," (Set (Var "KXN")) "," (Set (Var "KYP")) "," (Set (Var "KYN")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "O")) "," (Set (Var "I")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )  "st" (Bool (Bool (Set (Var "O"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "I"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "C0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  "}"  ) & (Bool (Set (Var "KXP"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q1")) where q1 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q1")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  "}"  ) & (Bool (Set (Var "KXN"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q2")) where q2 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q2")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  "}"  ) & (Bool (Set (Var "KYP"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q3")) where q3 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q3")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "q3"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q3"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  "}"  ) & (Bool (Set (Var "KYN"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q4")) where q4 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q4")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q4"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q4"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  "}"  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")))  ($#r2_hidden :::"in"::: )  (Set (Var "KXN"))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")))  ($#r2_hidden :::"in"::: )  (Set (Var "KXP"))) & (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")))  ($#r2_hidden :::"in"::: )  (Set (Var "KYP"))) & (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")))  ($#r2_hidden :::"in"::: )  (Set (Var "KYN"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0")))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g"))))))) ; 
 
theorem :: JGRAPH_5:14 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "C0")) "," (Set (Var "KXP")) "," (Set (Var "KXN")) "," (Set (Var "KYP")) "," (Set (Var "KYN")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "O")) "," (Set (Var "I")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )  "st" (Bool (Bool (Set (Var "O"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "I"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "C0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::">="::: )  (Num 1))  "}"  ) & (Bool (Set (Var "KXP"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q1")) where q1 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q1")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  "}"  ) & (Bool (Set (Var "KXN"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q2")) where q2 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q2")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  "}"  ) & (Bool (Set (Var "KYP"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q3")) where q3 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q3")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "q3"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q3"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  "}"  ) & (Bool (Set (Var "KYN"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q4")) where q4 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q4")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q4"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q4"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  "}"  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")))  ($#r2_hidden :::"in"::: )  (Set (Var "KXN"))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")))  ($#r2_hidden :::"in"::: )  (Set (Var "KXP"))) & (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")))  ($#r2_hidden :::"in"::: )  (Set (Var "KYN"))) & (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")))  ($#r2_hidden :::"in"::: )  (Set (Var "KYP"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0")))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g"))))))) ; 
 
theorem :: JGRAPH_5:15 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "C0")) "," (Set (Var "KXP")) "," (Set (Var "KXN")) "," (Set (Var "KYP")) "," (Set (Var "KYN")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "O")) "," (Set (Var "I")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )  "st" (Bool (Bool (Set (Var "O"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "I"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "C0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::">="::: )  (Num 1))  "}"  ) & (Bool (Set (Var "KXP"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q1")) where q1 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q1")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  "}"  ) & (Bool (Set (Var "KXN"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q2")) where q2 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q2")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  "}"  ) & (Bool (Set (Var "KYP"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q3")) where q3 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q3")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "q3"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q3"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  "}"  ) & (Bool (Set (Var "KYN"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q4")) where q4 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q4")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q4"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q4"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  "}"  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")))  ($#r2_hidden :::"in"::: )  (Set (Var "KXN"))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")))  ($#r2_hidden :::"in"::: )  (Set (Var "KXP"))) & (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")))  ($#r2_hidden :::"in"::: )  (Set (Var "KYP"))) & (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")))  ($#r2_hidden :::"in"::: )  (Set (Var "KYN"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0")))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g"))))))) ; 
 
theorem :: JGRAPH_5:16 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "C0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "C0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q")) where q "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::">="::: )  (Num 1))  "}"  ) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0")))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))))) ; 
 
theorem :: JGRAPH_5:17 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "C0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "C0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::">="::: )  (Num 1))  "}"  ) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p1")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p2")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p3")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p4")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "h"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "C0")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0"))) & (Bool (Set (Set (Var "h"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Set (Var "h"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p2")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Set (Var "h"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p3")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Set (Var "h"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p4")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")" ))) "holds"  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p1"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p3"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p4"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p2"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0")))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g"))))))) ; 
 begin  
theorem :: JGRAPH_5:18 (Bool  "for" (Set (Var "cn")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "cn"))) & (Bool (Set (Var "cn"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "cn"))  ($#k5_jgraph_4 :::"-FanMorphN"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 
theorem :: JGRAPH_5:19 (Bool  "for" (Set (Var "cn")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "cn"))) & (Bool (Set (Var "cn"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "cn"))  ($#k5_jgraph_4 :::"-FanMorphN"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 
theorem :: JGRAPH_5:20 (Bool  "for" (Set (Var "cn")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "cn"))) & (Bool (Set (Var "cn"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "cn"))) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "cn"))  ($#k5_jgraph_4 :::"-FanMorphN"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))) ; 
 
theorem :: JGRAPH_5:21 (Bool  "for" (Set (Var "cn")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "cn"))) & (Bool (Set (Var "cn"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q1")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q2")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q1")) ($#k12_euclid :::".|"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q2")) ($#k12_euclid :::".|"::: ) )))) "holds"  (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 "p1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "cn"))  ($#k5_jgraph_4 :::"-FanMorphN"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q1")))) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "cn"))  ($#k5_jgraph_4 :::"-FanMorphN"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q2"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p1")) ($#k12_euclid :::".|"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p2")) ($#k12_euclid :::".|"::: ) )))))) ; 
 
theorem :: JGRAPH_5:22 (Bool  "for" (Set (Var "sn")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "sn"))) & (Bool (Set (Var "sn"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sn"))  ($#k7_jgraph_4 :::"-FanMorphE"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 
theorem :: JGRAPH_5:23 (Bool  "for" (Set (Var "sn")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "sn"))) & (Bool (Set (Var "sn"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "sn"))) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sn"))  ($#k7_jgraph_4 :::"-FanMorphE"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))) ; 
 
theorem :: JGRAPH_5:24 (Bool  "for" (Set (Var "sn")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "sn"))) & (Bool (Set (Var "sn"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q1")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q2")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q1")) ($#k12_euclid :::".|"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q2")) ($#k12_euclid :::".|"::: ) )))) "holds"  (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 "p1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sn"))  ($#k7_jgraph_4 :::"-FanMorphE"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q1")))) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sn"))  ($#k7_jgraph_4 :::"-FanMorphE"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q2"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p1")) ($#k12_euclid :::".|"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p2")) ($#k12_euclid :::".|"::: ) )))))) ; 
 
theorem :: JGRAPH_5:25 (Bool  "for" (Set (Var "cn")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "cn"))) & (Bool (Set (Var "cn"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "cn"))  ($#k9_jgraph_4 :::"-FanMorphS"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 
theorem :: JGRAPH_5:26 (Bool  "for" (Set (Var "cn")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "cn"))) & (Bool (Set (Var "cn"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "cn")))) "holds"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "cn"))  ($#k9_jgraph_4 :::"-FanMorphS"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))) ; 
 
theorem :: JGRAPH_5:27 (Bool  "for" (Set (Var "cn")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "cn"))) & (Bool (Set (Var "cn"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q1")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q2")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q1")) ($#k12_euclid :::".|"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q2")) ($#k12_euclid :::".|"::: ) )))) "holds"  (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 "p1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "cn"))  ($#k9_jgraph_4 :::"-FanMorphS"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q1")))) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "cn"))  ($#k9_jgraph_4 :::"-FanMorphS"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q2"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p1")) ($#k12_euclid :::".|"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p2")) ($#k12_euclid :::".|"::: ) )))))) ; 
 begin  
theorem :: JGRAPH_5:28 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q")) where q "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  )) "holds"  (Bool  "("  (Bool (Set   ($#k6_pscomp_1 :::"W-bound"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) & (Bool (Set   ($#k8_pscomp_1 :::"E-bound"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k9_pscomp_1 :::"S-bound"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) & (Bool (Set   ($#k7_pscomp_1 :::"N-bound"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: JGRAPH_5:29 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q")) where q "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  )) "holds"  (Bool (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ))) ; 
 
theorem :: JGRAPH_5:30 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q")) where q "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  )) "holds"  (Bool (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ))) ; 
 
theorem :: JGRAPH_5:31 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) ; 
 
theorem :: JGRAPH_5:32 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) ; 
 
theorem :: JGRAPH_5:33 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q")) where q "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  )) "holds"  (Bool  "("  (Bool (Set   ($#k8_jordan6 :::"Upper_Arc"::: )  (Set (Var "P")))  ($#r1_tarski :::"c="::: )  (Set (Var "P"))) & (Bool (Set   ($#k9_jordan6 :::"Lower_Arc"::: )  (Set (Var "P")))  ($#r1_tarski :::"c="::: )  (Set (Var "P")))  ")" )) ; 
 
theorem :: JGRAPH_5:34 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q")) where q "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  )) "holds"  (Bool (Set   ($#k8_jordan6 :::"Upper_Arc"::: )  (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 "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  "}"  )) ; 
 
theorem :: JGRAPH_5:35 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q")) where q "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  )) "holds"  (Bool (Set   ($#k9_jordan6 :::"Lower_Arc"::: )  (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 "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  "}"  )) ; 
 
theorem :: JGRAPH_5:36 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set  "(" (Set  "(" (Set (Var "e"))  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "d")) ")" ) "," (Set  "(" (Set  "(" (Set (Var "e"))  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "d")) ")" ) ")"  ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "e"))  ($#k8_real_1 :::"*"::: )  (Set (Var "r")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "d"))))  ")" )  ")" ))) ; 
 
theorem :: JGRAPH_5:37 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set  "(" (Set  "(" (Set (Var "e"))  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "d")) ")" ) "," (Set  "(" (Set  "(" (Set (Var "e"))  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "d")) ")" ) ")"  ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "e"))  ($#k8_real_1 :::"*"::: )  (Set (Var "r")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "d"))))  ")" )  ")" ))) ; 
 
theorem :: JGRAPH_5:38 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "r")) ")" )  ($#k7_real_1 :::"+"::: )  (Num 1)))  ")" ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))  ")" )) ; 
 
theorem :: JGRAPH_5:39 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "r")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1)))  ")" ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: JGRAPH_5:40 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  )) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k9_jordan6 :::"Lower_Arc"::: )  (Set (Var "P")) ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (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   ($#k9_jordan6 :::"Lower_Arc"::: )  (Set (Var "P"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "P")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set (Var "P"))))  ")" ))) ; 
 
theorem :: JGRAPH_5:41 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  )) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k8_jordan6 :::"Upper_Arc"::: )  (Set (Var "P")) ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (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   ($#k8_jordan6 :::"Upper_Arc"::: )  (Set (Var "P"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "P")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set (Var "P"))))  ")" ))) ; 
 
theorem :: JGRAPH_5:42 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  )) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k9_jordan6 :::"Lower_Arc"::: )  (Set (Var "P")) ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r1")))  ($#r1_hidden :::"="::: )  (Set (Var "q1"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r2")))  ($#r1_hidden :::"="::: )  (Set (Var "q2"))) & (Bool (Set (Var "r1"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "r2"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "r1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r2"))) "iff" (Bool (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  ))  ")" ))  ")" ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set (Var "P")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "P"))))  ")" ))) ; 
 
theorem :: JGRAPH_5:43 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  )) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k8_jordan6 :::"Upper_Arc"::: )  (Set (Var "P")) ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r1")))  ($#r1_hidden :::"="::: )  (Set (Var "q1"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r2")))  ($#r1_hidden :::"="::: )  (Set (Var "q2"))) & (Bool (Set (Var "r1"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "r2"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "r1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r2"))) "iff" (Bool (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  ))  ")" ))  ")" ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "P")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set (Var "P"))))  ")" ))) ; 
 
theorem :: JGRAPH_5:44 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_jordan6 :::"Upper_Arc"::: )  (Set (Var "P")))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P")))) "holds"  (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_jordan6 :::"Upper_Arc"::: )  (Set (Var "P")))))) ; 
 
theorem :: JGRAPH_5:45 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  ))  ")" ))) ; 
 
theorem :: JGRAPH_5:46 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  ))  ")" ))) ; 
 
theorem :: JGRAPH_5:47 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )))) ; 
 
theorem :: JGRAPH_5:48 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "P"))))) "holds"  (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )))) ; 
 
theorem :: JGRAPH_5:49 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool  "("  (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool (Bool  "not" (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "holds"  (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: JGRAPH_5:50 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )))) ; 
 
theorem :: JGRAPH_5:51 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("  (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )) "or" (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  ))  ")" )) "holds"  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))))) ; 
 
theorem :: JGRAPH_5:52 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("  (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )) "or" (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  ))  ")" )) "holds"  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))))) ; 
 
theorem :: JGRAPH_5:53 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("  (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )) "or" (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  ))  ")" )) "holds"  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))))) ; 
 
theorem :: JGRAPH_5:54 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  ))) "holds"  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))))) ; 
 
theorem :: JGRAPH_5:55 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  ))) "holds"  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))))) ; 
 
theorem :: JGRAPH_5:56 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "P")))) & (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  ))) "holds"  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))))) ; 
 
theorem :: JGRAPH_5:57 (Bool  "for" (Set (Var "cn")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "cn"))) & (Bool (Set (Var "cn"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "cn"))  ($#k9_jgraph_4 :::"-FanMorphS"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 
theorem :: JGRAPH_5:58 (Bool  "for" (Set (Var "cn")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "cn"))) & (Bool (Set (Var "cn"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "cn"))  ($#k9_jgraph_4 :::"-FanMorphS"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "cn"))  ($#k9_jgraph_4 :::"-FanMorphS"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p2"))))) "holds"  (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P")))))) ; 
 
theorem :: JGRAPH_5:59 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p3"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p4"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )(Bool  "ex" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "q4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))  ")" ) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p2")))) & (Bool (Set (Var "q3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p3")))) & (Bool (Set (Var "q4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p4")))) & (Bool (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q3")) "," (Set (Var "q4")) "," (Set (Var "P")))  ")" ))))) ; 
 
theorem :: JGRAPH_5:60 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )(Bool  "ex" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "q4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))  ")" ) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p2")))) & (Bool (Set (Var "q3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p3")))) & (Bool (Set (Var "q4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p4")))) & (Bool (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q3")) "," (Set (Var "q4")) "," (Set (Var "P")))  ")" ))))) ; 
 
theorem :: JGRAPH_5:61 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )(Bool  "ex" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "q4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))  ")" ) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p2")))) & (Bool (Set (Var "q3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p3")))) & (Bool (Set (Var "q4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p4")))) & (Bool (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q3")) "," (Set (Var "q4")) "," (Set (Var "P")))  ")" ))))) ; 
 
theorem :: JGRAPH_5:62 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P"))) & (Bool  "("  (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) & (Bool  "("  (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) & (Bool  "("  (Bool (Set (Set (Var "p3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set (Var "p3"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) & (Bool  "("  (Bool (Set (Set (Var "p4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set (Var "p4"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )(Bool  "ex" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "q4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))  ")" ) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p2")))) & (Bool (Set (Var "q3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p3")))) & (Bool (Set (Var "q4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p4")))) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q3")) "," (Set (Var "q4")) "," (Set (Var "P")))  ")" ))))) ; 
 
theorem :: JGRAPH_5:63 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P"))) & (Bool  "("  (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) & (Bool  "("  (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) & (Bool  "("  (Bool (Set (Set (Var "p3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set (Var "p3"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) & (Bool  "("  (Bool (Set (Set (Var "p4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Set (Var "p4"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )(Bool  "ex" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "q4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))  ")" ) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p2")))) & (Bool (Set (Var "q3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p3")))) & (Bool (Set (Var "q4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p4")))) & (Bool (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q3")) "," (Set (Var "q4")) "," (Set (Var "P")))  ")" ))))) ; 
 
theorem :: JGRAPH_5:64 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool (Set (Var "p4"))  ($#r1_hidden :::"="::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "P")))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )(Bool  "ex" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "q4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))  ")" ) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p2")))) & (Bool (Set (Var "q3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p3")))) & (Bool (Set (Var "q4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p4")))) & (Bool (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q3")) "," (Set (Var "q4")) "," (Set (Var "P")))  ")" ))))) ; 
 
theorem :: JGRAPH_5:65 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )(Bool  "ex" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "q4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))  ")" ) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p2")))) & (Bool (Set (Var "q3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p3")))) & (Bool (Set (Var "q4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p4")))) & (Bool (Set (Set (Var "q1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q4"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "q3")) "," (Set (Var "q4")) "," (Set (Var "P")))  ")" ))))) ; 
 begin  
theorem :: JGRAPH_5:66 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p3"))) & (Bool (Set (Var "p3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p4"))) & (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p3"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p4"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "p3"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))  ")" ) & (Bool (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")))) & (Bool (Set  ($#k19_euclid :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p2")))) & (Bool (Set  ($#k19_euclid :::"|["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p3")))) & (Bool (Set  ($#k19_euclid :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) ($#k19_euclid :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p4"))))  ")" )))) ; 
 
theorem :: JGRAPH_5:67 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p3"))) & (Bool (Set (Var "p3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p4")))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))  ")" ) & (Bool (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")))) & (Bool (Set  ($#k19_euclid :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p2")))) & (Bool (Set  ($#k19_euclid :::"|["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p3")))) & (Bool (Set  ($#k19_euclid :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) ($#k19_euclid :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p4"))))  ")" )))) ; 
 
theorem :: JGRAPH_5:68 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "C0")) "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P")))) "holds"  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "C0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  "}"  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p1"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p3"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p2"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p4"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0")))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))))))) ; 
 
theorem :: JGRAPH_5:69 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "C0")) "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P")))) "holds"  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "C0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  "}"  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p1"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p3"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p4"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p2"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0")))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))))))) ; 
 
theorem :: JGRAPH_5:70 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "C0")) "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P")))) "holds"  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "C0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::">="::: )  (Num 1))  "}"  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p1"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p3"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p4"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p2"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0")))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))))))) ; 
 
theorem :: JGRAPH_5:71 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "C0")) "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 (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "P"))) & (Bool   ($#r1_jordan6 :::"LE"::: )  (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "P")))) "holds"  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "C0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::">="::: )  (Num 1))  "}"  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p1"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p3"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p2"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p4"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set (Var "C0")))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))))))) ;