:: JGRAPH_2  semantic presentation begin  






theorem :: JGRAPH_2:1 (Bool  "for" (Set (Var "T1")) "," (Set (Var "S")) "," (Set (Var "T2")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "S"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T2")) "," (Set (Var "S"))  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "T1")) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))) & (Bool (Set (Var "T2")) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))) & (Bool (Set (Var "F1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T1")))) & (Bool (Set (Var "F2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T2")))) & (Bool (Set (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T1")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")))) & (Bool (Set (Var "F1")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "F2")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool  "("   "for" (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T1")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T2")) ")" )))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p"))))  ")" )) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g")))) & (Bool (Set (Var "h")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))))) ; 
 
theorem :: JGRAPH_2:2 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Var "q2")))) "holds"  (Bool (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "q2")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q3")) where q3 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "q"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "q3")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  "}"  ))))) ; 
 
theorem :: JGRAPH_2:3 (Bool  "("  (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) ; 
 
theorem :: JGRAPH_2:4 (Bool (Set   ($#k22_euclid :::"1.REAL"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ; 
 
theorem :: JGRAPH_2:5 (Bool  "("  (Bool (Set (Set  "("  ($#k22_euclid :::"1.REAL"::: )  (Num 2) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set  "("  ($#k22_euclid :::"1.REAL"::: )  (Num 2) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Num 1))  ")" ) ; 
 
theorem :: JGRAPH_2:6 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  ($#k4_pscomp_1 :::"proj1"::: ) ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  ($#k4_pscomp_1 :::"proj1"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_euclid :::"REAL"::: )  (Num 2)))  ")" ) ; 
 
theorem :: JGRAPH_2:7 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  ($#k5_pscomp_1 :::"proj2"::: ) ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  ($#k5_pscomp_1 :::"proj2"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_euclid :::"REAL"::: )  (Num 2)))  ")" ) ; 
 
theorem :: JGRAPH_2:8 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" ) "," (Set  "(" (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" ) ($#k19_euclid :::"]|"::: ) ))) ; 
 
theorem :: JGRAPH_2:9 (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) ($#k6_domain_1 :::"}"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "B"))  ($#k3_subset_1 :::"`"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))  ($#k6_subset_1 :::"\"::: )  (Set (Var "B")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: JGRAPH_2:10 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set (Var "V"))) & (Bool (Set (Var "V")) "is"   ($#v3_pre_topc :::"open"::: )  )) "holds"  (Bool  "ex" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "W")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "W")))  ($#r1_tarski :::"c="::: )  (Set (Var "V")))  ")" ))))  ")" ))) ; 
 
theorem :: JGRAPH_2:11 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "G")))) "holds"  (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "{"  (Set (Var "q")) where q "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "r")))) & (Bool (Set (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "r"))))  ")" )  "}"    ($#r1_tarski :::"c="::: )  (Set (Var "G")))  ")" )))) ; 
 
theorem :: JGRAPH_2:12 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y"))  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Z"))  (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  "(" (Set (Var "Y"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "B")) ")" ) "," (Set  "(" (Set (Var "Z"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "C")) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "h")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "st"  (Bool  "("  (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "h"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f"))))  ")" ))))))) ; 
 



definitionfunc  :::"Out_In_Sq":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) "," (Set  "("  ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) means :: JGRAPH_2:def 1 (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   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) "holds"  (Bool  "("   "("  (Bool (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  ")" )) "implies" (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")"  & (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" ) "or" (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" ) "," (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")" )  ")" )); end; 




:: deftheorem    defines :::"Out_In_Sq"::: JGRAPH_2:def 1 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) "," (Set  "("  ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_jgraph_2 :::"Out_In_Sq"::: )  )) "iff" (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   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) "holds"  (Bool  "("   "("  (Bool (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  ")" )) "implies" (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")"  & (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" ) "or" (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" ) "," (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")" )  ")" ))  ")" )); 
 
theorem :: JGRAPH_2:13 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )))  ")" )  ")" )) ; 
 
theorem :: JGRAPH_2:14 (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   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) "holds"  (Bool  "("   "("  (Bool (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )))  ")" )  ")" )) "implies" (Bool (Set (Set  ($#k1_jgraph_2 :::"Out_In_Sq"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" ) "," (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")"  & (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )))  ")" ) "or" (Bool (Set (Set  ($#k1_jgraph_2 :::"Out_In_Sq"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")" )  ")" )) ; 
 
theorem :: JGRAPH_2:15 (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "K0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "D")) ")" )  "st" (Bool (Bool (Set (Var "K0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  ")" ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))  ")" )  "}"  )) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set  ($#k1_jgraph_2 :::"Out_In_Sq"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "K0")) ")" ))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "D")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ))))) ; 
 
theorem :: JGRAPH_2:16 (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "K0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "D")) ")" )  "st" (Bool (Bool (Set (Var "K0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )))  ")" )  ")" ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))  ")" )  "}"  )) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set  ($#k1_jgraph_2 :::"Out_In_Sq"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "K0")) ")" ))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "D")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ))))) ; 
 
theorem :: JGRAPH_2:17 (Bool  "for" (Set (Var "K0a")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "K0a"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  ")" ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))  ")" )  "}"  ) & (Bool (Set (Set (Var "D"))  ($#k3_subset_1 :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) ($#k6_domain_1 :::"}"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "K0a")) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "D")) ")" )) & (Bool (Set (Var "K0a")) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))  ")" ))) ; 
 
theorem :: JGRAPH_2:18 (Bool  "for" (Set (Var "K0a")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "K0a"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )))  ")" )  ")" ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))  ")" )  "}"  ) & (Bool (Set (Set (Var "D"))  ($#k3_subset_1 :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) ($#k6_domain_1 :::"}"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "K0a")) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "D")) ")" )) & (Bool (Set (Var "K0a")) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))  ")" ))) ; 
 
theorem :: JGRAPH_2:19 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r1"))) & (Bool (Set (Set (Var "f2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r2")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "r2")))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_2:20 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_2:21 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r1"))) & (Bool (Set (Set (Var "f2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r2")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r2")))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_2:22 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "r1")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r1")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r1")))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_2:23 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "r1")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r1")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r1")))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" ))))) ; 
 
theorem :: JGRAPH_2:24 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "r1")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r1")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a")))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" ))))) ; 
 
theorem :: JGRAPH_2:25 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r1"))) & (Bool (Set (Set (Var "f2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r2")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r2")))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_2:26 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool  "("   "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "holds" (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "r1")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r1")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "r1")))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_2:27 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool  "("   "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "holds" (Bool (Set (Set (Var "f2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r1"))) & (Bool (Set (Set (Var "f2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r2")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r1"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "r2")))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_2:28 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool  "("   "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "holds" (Bool (Set (Set (Var "f2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r1"))) & (Bool (Set (Set (Var "f2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "r2")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r1"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "r2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "r2")))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_2:29 (Bool  "for" (Set (Var "K0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "p"))))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: JGRAPH_2:30 (Bool  "for" (Set (Var "K0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "p"))))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: JGRAPH_2:31 (Bool  "for" (Set (Var "K1")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K1")) ")" ) "," (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) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K1")) ")" )))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" ) & (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  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K1")) ")" )))) "holds"  (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: JGRAPH_2:32 (Bool  "for" (Set (Var "K1")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K1")) ")" ) "," (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) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K1")) ")" )))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )))  ")" ) & (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  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K1")) ")" )))) "holds"  (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: JGRAPH_2:33 (Bool  "for" (Set (Var "K1")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K1")) ")" ) "," (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) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K1")) ")" )))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" ) & (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  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K1")) ")" )))) "holds"  (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: JGRAPH_2:34 (Bool  "for" (Set (Var "K1")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K1")) ")" ) "," (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) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K1")) ")" )))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )))  ")" ) & (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  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K1")) ")" )))) "holds"  (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: JGRAPH_2:35 (Bool  "for" (Set (Var "K0")) "," (Set (Var "B0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B0")) ")" )  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "K0"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "B0"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set  ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "K0"))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) )))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )))) ; 
 
theorem :: JGRAPH_2:36 (Bool  "for" (Set (Var "K0")) "," (Set (Var "B0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B0")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_jgraph_2 :::"Out_In_Sq"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "K0")))) & (Bool (Set (Var "B0"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) & (Bool (Set (Var "K0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  ")" ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))  ")" )  "}"  )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: JGRAPH_2:37 (Bool  "for" (Set (Var "K0")) "," (Set (Var "B0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B0")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_jgraph_2 :::"Out_In_Sq"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "K0")))) & (Bool (Set (Var "B0"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) & (Bool (Set (Var "K0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )))  ")" )  ")" ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))  ")" )  "}"  )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 scheme  :: JGRAPH_2:sch 1 TopSubset{ P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool P1[(Set (Var "p"))])  "}"   "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))
 proof 


end; scheme  :: JGRAPH_2:sch 2 TopCompl{ P1[   ($#m1_hidden :::"set"::: )  ], F1() ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) } : 
(Bool (Set (Set F1 "("  ")" )  ($#k3_subset_1 :::"`"::: )  )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool P1[(Set (Var "p"))])  "}"  )
 provided
(Bool (Set F1 "("  ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool P1[(Set (Var "p"))])  "}"  )
 proof 


end; scheme  :: JGRAPH_2:sch 3 ClosedSubset{ F1(  ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )) ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  , F2(  ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )) ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   } : 
(Bool  "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set F1 "(" (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set F2 "(" (Set (Var "p")) ")" ))  "}"   "is"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))
 provided
(Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set F1 "(" (Set  "(" (Set (Var "p"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "q")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set F1 "(" (Set (Var "p")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set F1 "(" (Set (Var "q")) ")" ))) & (Bool (Set F2 "(" (Set  "(" (Set (Var "p"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "q")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set F2 "(" (Set (Var "p")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set F2 "(" (Set (Var "q")) ")" )))  ")" ))
 and  
(Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "p"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set F1 "(" (Set  "(" (Set (Var "p"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "q")) ")" ) ")" )  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set F2 "(" (Set  "(" (Set (Var "p"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "q")) ")" ) ")" )  ($#k3_square_1 :::"^2"::: )  ")" ))))
 proof 


end; 
theorem :: JGRAPH_2:38 (Bool  "for" (Set (Var "B0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "K0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B0")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B0")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B0")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_jgraph_2 :::"Out_In_Sq"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "K0")))) & (Bool (Set (Var "B0"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) & (Bool (Set (Var "K0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )))  ")" )  ")" ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))  ")" )  "}"  )) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "K0")) "is"   ($#v4_pre_topc :::"closed"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_2:39 (Bool  "for" (Set (Var "B0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "K0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B0")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B0")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B0")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_jgraph_2 :::"Out_In_Sq"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "K0")))) & (Bool (Set (Var "B0"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) & (Bool (Set (Var "K0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )))  ")" )  ")" ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))  ")" )  "}"  )) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "K0")) "is"   ($#v4_pre_topc :::"closed"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_2:40 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Set (Var "D"))  ($#k3_subset_1 :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) ($#k6_domain_1 :::"}"::: ) ))) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "D")) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "D")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_jgraph_2 :::"Out_In_Sq"::: )  )) & (Bool (Set (Var "h")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" ))) ; 
 
theorem :: JGRAPH_2:41 (Bool  "for" (Set (Var "B")) "," (Set (Var "K0")) "," (Set (Var "Kb")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Var "K0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (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))  ")" )  "}"  ) & (Bool (Set (Var "Kb"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q")) where q "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool  "("  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" ) "or" (Bool  "("  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" ) "or" (Bool  "("  (Bool (Num 1)  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" )  ")" )  "}"  )) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "(" (Set (Var "B"))  ($#k3_subset_1 :::"`"::: )  ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "(" (Set (Var "B"))  ($#k3_subset_1 :::"`"::: )  ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set (Var "K0"))) & (Bool (Set (Var "t"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) "holds"  (Bool  "not" (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "t")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "K0"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Kb")))))  ")" ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Bool  "not" (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "K0"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Kb")))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r")))  ($#r2_hidden :::"in"::: )  (Set (Var "K0")))  ")" ) & (Bool  "("   "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Var "Kb")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Var "s")))  ")" )  ")" ))) ; 
 
theorem :: JGRAPH_2:42 (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 "K0")) "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 "K0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (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))  ")" )  "}"  ) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#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 :::"<="::: )  (Num 1)) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#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 :::"<="::: )  (Num 1)) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#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 :::"<="::: )  (Num 1)) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#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 :::"<="::: )  (Num 1)) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "K0"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "K0")))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g"))))))) ; 
 
theorem :: JGRAPH_2:43 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (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  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "A"))  ($#k4_real_1 :::"*"::: )  (Set  "(" (Set (Var "t"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "B")) ")" ) "," (Set  "(" (Set  "(" (Set (Var "C"))  ($#k4_real_1 :::"*"::: )  (Set  "(" (Set (Var "t"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "D")) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 definitionlet "A", "B", "C", "D" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"AffineMap":::  "(" "A" "," "B" "," "C" "," "D" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) means :: JGRAPH_2:def 2 (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" "A"  ($#k4_real_1 :::"*"::: )  (Set  "(" (Set (Var "t"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  "B" ")" ) "," (Set  "(" (Set  "(" "C"  ($#k4_real_1 :::"*"::: )  (Set  "(" (Set (Var "t"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  "D" ")" ) ($#k19_euclid :::"]|"::: ) ))); end; 








:: deftheorem    defines :::"AffineMap"::: JGRAPH_2:def 2 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_jgraph_2 :::"AffineMap"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ")" )) "iff" (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set (Var "b5"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "A"))  ($#k4_real_1 :::"*"::: )  (Set  "(" (Set (Var "t"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "B")) ")" ) "," (Set  "(" (Set  "(" (Set (Var "C"))  ($#k4_real_1 :::"*"::: )  (Set  "(" (Set (Var "t"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "D")) ")" ) ($#k19_euclid :::"]|"::: ) )))  ")" ))); 
 registrationlet "a", "b", "c", "d" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k2_jgraph_2 :::"AffineMap"::: )   "(" "a" "," "b" "," "c" "," "d" ")" ) ->   ($#v5_pre_topc :::"continuous"::: )   ; 
end; 
theorem :: JGRAPH_2:44 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "C"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k2_jgraph_2 :::"AffineMap"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ")" ) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) ; 
 
theorem :: JGRAPH_2:45 (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"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (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 (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (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 "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 (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 (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 "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 (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 (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d"))) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )  "holds"  (Bool  "("   "not" (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k17_euclid :::"`1"::: )  )) "or"  "not" (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) "or"  "not" (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k18_euclid :::"`2"::: )  )) "or"  "not" (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d")))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )  "holds"  (Bool  "("   "not" (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k17_euclid :::"`1"::: )  )) "or"  "not" (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) "or"  "not" (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k18_euclid :::"`2"::: )  )) "or"  "not" (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_2:46 (Bool  "("  (Bool  "{"  (Set (Var "p7")) where p7 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set (Set (Var "p7"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p7"))  ($#k17_euclid :::"`1"::: )  ))  "}"   "is"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )) & (Bool  "{"  (Set (Var "p7")) where p7 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set (Set (Var "p7"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p7"))  ($#k18_euclid :::"`2"::: )  ))  "}"   "is"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))  ")" ) ; 
 
theorem :: JGRAPH_2:47 (Bool  "("  (Bool  "{"  (Set (Var "p7")) where p7 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p7"))  ($#k17_euclid :::"`1"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p7"))  ($#k18_euclid :::"`2"::: )  ))  "}"   "is"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )) & (Bool  "{"  (Set (Var "p7")) where p7 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set (Set (Var "p7"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p7"))  ($#k17_euclid :::"`1"::: )  ")" )))  "}"   "is"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))  ")" ) ; 
 
theorem :: JGRAPH_2:48 (Bool  "("  (Bool  "{"  (Set (Var "p7")) where p7 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p7"))  ($#k18_euclid :::"`2"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p7"))  ($#k17_euclid :::"`1"::: )  ))  "}"   "is"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )) & (Bool  "{"  (Set (Var "p7")) where p7 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set (Set (Var "p7"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p7"))  ($#k18_euclid :::"`2"::: )  ")" )))  "}"   "is"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))  ")" ) ;