:: TOPMETR2  semantic presentation begin  













theorem :: TOPMETR2:1 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool  "("   "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "x2"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")) ")" )))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x1")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x2"))))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) ; 
 
theorem :: TOPMETR2:2 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")) ")" ) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g")) ")" )))) ; 
 



theorem :: TOPMETR2:3 (Bool  "for" (Set (Var "T")) "being"   ($#v8_pre_topc :::"T_2"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "P")) ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "Q")) ")" )  "st" (Bool (Bool (Set (Set (Var "P"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Q")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set (Var "g")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set  "(" (Set (Var "P"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Q")) ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1)))  ")" ))))))) ;