:: JGRAPH_3  semantic presentation begin  



theorem :: JGRAPH_3:1 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ))) & (Bool (Set (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k5_square_1 :::"^2"::: )  ")" )))  ")" )) ; 
 
theorem :: JGRAPH_3:2 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "B")) ")" )  ($#k7_relat_1 :::".:"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set  "(" (Set (Var "C"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "B")) ")" ))))) ; 
 
theorem :: JGRAPH_3:3 (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 "p0")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Set (Var "D"))  ($#k3_subset_1 :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "p0")) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Set (Var "E"))  ($#k3_subset_1 :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p0")) ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Var "X")) "is"   ($#v8_pre_topc :::"T_2"::: )  ) & (Bool (Set (Var "Y")) "is"   ($#v8_pre_topc :::"T_2"::: )  ) & (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "D")) ")" )  "holds" (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p0"))))  ")" ) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "D"))) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "D")) ")" ) "," (Set  "(" (Set (Var "Y"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "E")) ")" )) & (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 "p0")))  ($#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 "p0"))  ($#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")))  ")" ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )))))) ; 
 begin  



definitionfunc  :::"Sq_Circ":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )) means :: JGRAPH_3:def 1 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) "implies" (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p")))  ")"  &  "("  (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) ")" )))) "implies" (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) ($#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"  "not" (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) "or" (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")" )  ")" )); end; 




:: deftheorem    defines :::"Sq_Circ"::: JGRAPH_3:def 1 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_jgraph_3 :::"Sq_Circ"::: )  )) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) "implies" (Bool (Set (Set (Var "b1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p")))  ")"  &  "("  (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) ")" )))) "implies" (Bool (Set (Set (Var "b1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) ($#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"  "not" (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) "or" (Bool (Set (Set (Var "b1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")" )  ")" ))  ")" )); 
 
theorem :: JGRAPH_3:4 (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_3 :::"Sq_Circ"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^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_3 :::"Sq_Circ"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")" )  ")" )) ; 
 
theorem :: JGRAPH_3:5 (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")) (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">="::: )  (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   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "r1")))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_3:6 (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")) ")" )  ($#k3_square_1 :::"^2"::: )  )))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_3:7 (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 (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "r2")) ")" )  ($#k3_square_1 :::"^2"::: )  ")" ))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_3:8 (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   ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "r2")) ")" )  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_3:9 (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"))  ($#k6_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "r2")) ")" )  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" ))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_3:10 (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 "r2"))  ($#k6_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "r2")) ")" )  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" ))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_3:11 (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 (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^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"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: JGRAPH_3:12 (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 (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^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"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: JGRAPH_3:13 (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 (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^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_3:14 (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 (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^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_3:15 (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_3 :::"Sq_Circ"::: ) )  ($#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_3:16 (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_3 :::"Sq_Circ"::: ) )  ($#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_3:sch 1 TopIncl{ P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool P1[(Set (Var "p"))]) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))  ")" )  "}"    ($#r1_tarski :::"c="::: )  (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))
 proof 


end; scheme  :: JGRAPH_3:sch 2 TopInter{ P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool  "("  (Bool P1[(Set (Var "p"))]) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))  ")" )  "}"    ($#r1_hidden :::"="::: )  (Set  "{"  (Set (Var "p7")) where p7 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool P1[(Set (Var "p7"))])  "}"    ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" )))
 proof 


end; 
theorem :: JGRAPH_3:17 (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_3 :::"Sq_Circ"::: ) )  ($#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_3:18 (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_3 :::"Sq_Circ"::: ) )  ($#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_3:19 (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 (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "D")))) & (Bool (Set (Var "h")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" ))) ; 
 
theorem :: JGRAPH_3:20 (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 "D"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) "holds"  (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 :::"}"::: ) ))) ; 
 
theorem :: JGRAPH_3:21 (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"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k1_jgraph_3 :::"Sq_Circ"::: )  )) & (Bool (Set (Var "h")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )) ; 
 
theorem :: JGRAPH_3:22 (Bool (Set   ($#k1_jgraph_3 :::"Sq_Circ"::: )  ) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) ; 
 registration
cluster (Set   ($#k1_jgraph_3 :::"Sq_Circ"::: )  ) ->   ($#v2_funct_1 :::"one-to-one"::: )   ; 
end; 
theorem :: JGRAPH_3:23 (Bool  "for" (Set (Var "Kb")) "," (Set (Var "Cb")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (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))  ")" )  ")" )  "}"  ) & (Bool (Set (Var "Cb"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p2")) where p2 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p2")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))  "}"  )) "holds"  (Bool (Set (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set (Var "Kb")))  ($#r1_hidden :::"="::: )  (Set (Var "Cb")))) ; 
 
theorem :: JGRAPH_3:24 (Bool  "for" (Set (Var "P")) "," (Set (Var "Kb")) "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 "Kb")) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "P")) ")" )  "st" (Bool (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))  ")" )  ")" )  "}"  ) & (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )) "holds"  (Bool (Set (Var "P")) "is"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )  ))) ; 
 
theorem :: JGRAPH_3:25 (Bool  "for" (Set (Var "Kb")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (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  "("  (Bool (Set (Var "Kb")) "is"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )  ) & (Bool (Set (Var "Kb")) "is"   ($#v2_compts_1 :::"compact"::: )  )  ")" )) ; 
 
theorem :: JGRAPH_3:26 (Bool  "for" (Set (Var "Cb")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "Cb"))  ($#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 (Set (Var "Cb")) "is"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )  )) ; 
 begin  
theorem :: JGRAPH_3:27 (Bool  "for" (Set (Var "K0")) "," (Set (Var "C0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "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 (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 "C0"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p1")) where p1 "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p1")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  "}"  )) "holds"  (Bool (Set (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k8_relset_1 :::"""::: )  (Set (Var "C0")))  ($#r1_tarski :::"c="::: )  (Set (Var "K0")))) ; 
 
theorem :: JGRAPH_3:28 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) "implies" (Bool (Set (Set  "(" (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_funct_1 :::"""::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (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) ")" )))) "implies" (Bool (Set (Set  "(" (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_funct_1 :::"""::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) ($#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  "(" (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_funct_1 :::"""::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")" )  ")" )) ; 
 
theorem :: JGRAPH_3:29 (Bool (Set (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_funct_1 :::"""::: )  ) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )) ; 
 
theorem :: JGRAPH_3:30 (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  "(" (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_funct_1 :::"""::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^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  "(" (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_funct_1 :::"""::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")" )  ")" )) ; 
 
theorem :: JGRAPH_3:31 (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"))  ($#k4_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "r2")) ")" )  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" ))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_3:32 (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 "r2"))  ($#k4_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "r2")) ")" )  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" ))))  ")" ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: JGRAPH_3: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 (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^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"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: JGRAPH_3: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 (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^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"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: JGRAPH_3:35 (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 (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^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_3:36 (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 (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^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_3: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  "(" (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_funct_1 :::"""::: )  ")" )  ($#k5_relat_1 :::"|"::: )  (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_3:38 (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  "(" (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_funct_1 :::"""::: )  ")" )  ($#k5_relat_1 :::"|"::: )  (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"::: )  ))) ; 
 
theorem :: JGRAPH_3: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  "(" (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_funct_1 :::"""::: )  ")" )  ($#k5_relat_1 :::"|"::: )  (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_3:40 (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  "(" (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_funct_1 :::"""::: )  ")" )  ($#k5_relat_1 :::"|"::: )  (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_3:41 (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 (Set  "(" (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_funct_1 :::"""::: )  ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "D")))) & (Bool (Set (Var "h")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" ))) ; 
 
theorem :: JGRAPH_3:42 (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"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) )  ($#k2_funct_1 :::"""::: )  )) & (Bool (Set (Var "h")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" )) ; 
 
theorem :: JGRAPH_3:43 (Bool  "("  (Bool (Set   ($#k1_jgraph_3 :::"Sq_Circ"::: )  ) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  ($#k1_jgraph_3 :::"Sq_Circ"::: ) ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) & (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 (Set (Var "f"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k1_jgraph_3 :::"Sq_Circ"::: )  ))) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )  ")" )  ")" ) ; 
 
theorem :: JGRAPH_3:44 (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"))))))) ;