:: TOPGEN_3  semantic presentation begin  




definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "B" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "B" is  :::"point-filtered":::  means :: TOPGEN_3:def 1 (Bool  "for" (Set (Var "x")) "," (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "U1"))  ($#r2_hidden :::"in"::: )  "B") & (Bool (Set (Var "U2"))  ($#r2_hidden :::"in"::: )  "B") & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "U1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "U2"))))) "holds"  (Bool  "ex" (Set (Var "U")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X" "st"  (Bool  "("  (Bool (Set (Var "U"))  ($#r2_hidden :::"in"::: )  "B") & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "U"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "U1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "U2"))))  ")" ))); end; 





:: deftheorem    defines :::"point-filtered"::: TOPGEN_3:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v1_topgen_3 :::"point-filtered"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "U1"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "U2"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "U1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "U2"))))) "holds"  (Bool  "ex" (Set (Var "U")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "U"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "U"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "U1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "U2"))))  ")" )))  ")" ))); 
 
theorem :: TOPGEN_3:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v3_abian :::"covering"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "ex" (Set (Var "U")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "U"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))  ")" )))  ")" ))) ; 
 
theorem :: TOPGEN_3:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "B")) "is"   ($#v1_topgen_3 :::"point-filtered"::: )  ) & (Bool (Set (Var "B")) "is"   ($#v3_abian :::"covering"::: )  )) "holds"  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set (Var "B"))))) "holds"  (Bool  "("  (Bool (Set (Var "T")) "is"   ($#l1_pre_topc :::"TopSpace":::)) & (Bool (Set (Var "B")) "is"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")))  ")" )))) ; 
 
theorem :: TOPGEN_3:3 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#v2_relat_1 :::"non-empty"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "B")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "U")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "U"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "B"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))  ")" ) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "U")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "U"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "B"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "ex" (Set (Var "V")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "B"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Var "U")))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "U1"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "B"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Var "U2"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "B"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))) "holds"  (Bool  "ex" (Set (Var "U")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "U"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "B"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Var "U"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "U1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "U2"))))  ")" ))  ")" )) "holds"  (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set (Var "B")))) & (Bool  "("   "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set (Var "P"))))) "holds"  (Bool  "("  (Bool (Set (Var "T")) "is"   ($#l1_pre_topc :::"TopSpace":::)) & (Bool  "("   "for" (Set (Var "T9")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "T9"))  ($#r1_hidden :::"="::: )  (Set (Var "T")))) "holds"  (Bool (Set (Var "B")) "is"    ($#m1_topgen_2 :::"Neighborhood_System"::: )   "of" (Set (Var "T9")))  ")" )  ")" )  ")" )  ")" )))) ; 
 
theorem :: TOPGEN_3:4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k11_arytm_3 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" ) & (Bool  "("   "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "F")))) "holds"  (Bool (Set   ($#k8_setfam_1 :::"Intersect"::: )  (Set (Var "G")))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" )) "holds"  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_setfam_1 :::"COMPLEMENT"::: )  (Set (Var "F"))))) "holds"  (Bool  "("  (Bool (Set (Var "T")) "is"   ($#l1_pre_topc :::"TopSpace":::)) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ) "iff" (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" )  ")" )  ")" )))) ; 
 scheme  :: TOPGEN_3:sch 1 TopDefByClosedPred{ F1() ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "T")) "being"   ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ) "iff" (Bool P1[(Set (Var "A"))])  ")" )  ")" )  ")" ))
 provided
(Bool  "("  (Bool P1[(Set   ($#k11_arytm_3 :::"{}"::: )  )]) & (Bool P1[(Set F1 "("  ")" )])  ")" )
 and  
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool P1[(Set (Var "A"))]) & (Bool P1[(Set (Var "B"))])) "holds"  (Bool P1[(Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")))]))
 and  
(Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "G")))) "holds"  (Bool P1[(Set (Var "A"))])  ")" )) "holds"  (Bool P1[(Set   ($#k8_setfam_1 :::"Intersect"::: )  (Set (Var "G")))]))
 proof 


end; 
theorem :: TOPGEN_3:5 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool  "("   "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1"))) "iff" (Bool (Set (Var "A")) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2")))  ")" )  ")" )) "holds"  (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T1"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T2"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T2"))) "#)" ))) ; 
 
theorem :: TOPGEN_3:6 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool  "("   "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1"))) "iff" (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2")))  ")" )  ")" )) "holds"  (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T1"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T2"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T2"))) "#)" ))) ; 
 definitionlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; let "r" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Const "Y")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"rng"::: redefine func  :::"rng"::: "r" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "Y"; end; 
theorem :: TOPGEN_3:7 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Set (Var "c"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k11_arytm_3 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "c"))  ($#k3_funct_2 :::"."::: )  (Set (Var "A"))))  ")" ) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "c"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "c"))  ($#k3_funct_2 :::"."::: )  (Set (Var "A")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "c"))  ($#k3_funct_2 :::"."::: )  (Set (Var "B")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "c"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "c"))  ($#k3_funct_2 :::"."::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k3_funct_2 :::"."::: )  (Set (Var "A"))))  ")" )) "holds"  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_setfam_1 :::"COMPLEMENT"::: )  (Set  "("  ($#k1_topgen_3 :::"rng"::: )  (Set (Var "c")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "T")) "is"   ($#l1_pre_topc :::"TopSpace":::)) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A"))))  ")" )  ")" )))) ; 
 scheme  :: TOPGEN_3:sch 2 TopDefByClosureOp{ F1() ->    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "T")) "being"   ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) ")" ))  ")" )  ")" ))
 provided
(Bool (Set F2 "(" (Set  ($#k11_arytm_3 :::"{}"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "("  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set F2 "(" (Set (Var "A")) ")" )) & (Bool (Set F2 "(" (Set (Var "A")) ")" )  ($#r1_tarski :::"c="::: )  (Set F1 "("  ")" ))  ")" ))
 and  
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set F2 "(" (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set F2 "(" (Set (Var "A")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set F2 "(" (Set (Var "B")) ")" ))))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set F2 "(" (Set F2 "(" (Set (Var "A")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) ")" )))
 proof 


end; 
theorem :: TOPGEN_3:8 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T2")))) & (Bool  "("   "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1"))  (Bool  "for" (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2"))  "st" (Bool (Bool (Set (Var "A1"))  ($#r1_hidden :::"="::: )  (Set (Var "A2")))) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A1")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A2")))))  ")" )) "holds"  (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T2"))))) ; 
 
theorem :: TOPGEN_3:9 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Set (Var "i"))  ($#k1_funct_1 :::"."::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "i"))  ($#k3_funct_2 :::"."::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" ) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "i"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "i"))  ($#k3_funct_2 :::"."::: )  (Set (Var "A")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "i"))  ($#k3_funct_2 :::"."::: )  (Set (Var "B")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "i"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k3_funct_2 :::"."::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k3_funct_2 :::"."::: )  (Set (Var "A"))))  ")" )) "holds"  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_topgen_3 :::"rng"::: )  (Set (Var "i"))))) "holds"  (Bool  "("  (Bool (Set (Var "T")) "is"   ($#l1_pre_topc :::"TopSpace":::)) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A"))))  ")" )  ")" )))) ; 
 scheme  :: TOPGEN_3:sch 3 TopDefByInteriorOp{ F1() ->    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "T")) "being"   ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) ")" ))  ")" )  ")" ))
 provided
(Bool (Set F2 "(" (Set F1 "("  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" ))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set F2 "(" (Set (Var "A")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "A"))))
 and  
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set F2 "(" (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set F2 "(" (Set (Var "A")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set F2 "(" (Set (Var "B")) ")" ))))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set F2 "(" (Set F2 "(" (Set (Var "A")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) ")" )))
 proof 


end; 
theorem :: TOPGEN_3:10 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T2")))) & (Bool  "("   "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1"))  (Bool  "for" (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2"))  "st" (Bool (Bool (Set (Var "A1"))  ($#r1_hidden :::"="::: )  (Set (Var "A2")))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A2")))))  ")" )) "holds"  (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T2"))))) ; 
 begin  definitionfunc  :::"Sorgenfrey-line":::  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) means :: TOPGEN_3:def 2 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set (Var "B")))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "q")) ($#k3_rcomp_1 :::".["::: ) ) where x, q "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) : (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) & (Bool (Set (Var "q")) "is"   ($#v1_rat_1 :::"rational"::: )  )  ")" )  "}"  )  ")" ))  ")" ); end; 




:: deftheorem    defines :::"Sorgenfrey-line"::: TOPGEN_3:def 2 :  (Bool  "for" (Set (Var "b1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topgen_3 :::"Sorgenfrey-line"::: )  )) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "b1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set (Var "B")))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "q")) ($#k3_rcomp_1 :::".["::: ) ) where x, q "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) : (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) & (Bool (Set (Var "q")) "is"   ($#v1_rat_1 :::"rational"::: )  )  ")" )  "}"  )  ")" ))  ")" )  ")" )); 
 
theorem :: TOPGEN_3:11 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k3_rcomp_1 :::".["::: ) ) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ))) ; 
 
theorem :: TOPGEN_3:12 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_rcomp_1 :::".["::: ) ) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ))) ; 
 
theorem :: TOPGEN_3:13 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "x"))) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ))) ; 
 
theorem :: TOPGEN_3:14 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "x"))) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ))) ; 
 
theorem :: TOPGEN_3:15 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k2_limfunc1 :::"right_closed_halfline"::: )  (Set (Var "x"))) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ))) ; 
 
theorem :: TOPGEN_3:16 (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k4_numbers :::"INT"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) ; 
 
theorem :: TOPGEN_3:17 (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k3_numbers :::"RAT"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) ; 
 
theorem :: TOPGEN_3:18 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_taxonom2 :::"mutually-disjoint"::: )  ) & (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "a")))  ")" ))  ")" )) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_card_3 :::"countable"::: )  )) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; pred "x" :::"is_local_minimum_of"::: "X" means :: TOPGEN_3:def 3 (Bool  "("  (Bool "x"  ($#r2_hidden :::"in"::: )  "X") & (Bool  "ex" (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<"::: )  "x") & (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "y")) "," "x" ($#k2_rcomp_1 :::".["::: ) )  ($#r1_xboole_0 :::"misses"::: )  "X")  ")" ))  ")" ); end; 





:: deftheorem    defines :::"is_local_minimum_of"::: TOPGEN_3:def 3 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_topgen_3 :::"is_local_minimum_of"::: )  (Set (Var "X"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool  "ex" (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X")))  ")" ))  ")" )  ")" ))); 
 
theorem :: TOPGEN_3:19 (Bool  "for" (Set (Var "U")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool  "{"  (Set (Var "x")) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) : (Bool (Set (Var "x"))  ($#r1_topgen_3 :::"is_local_minimum_of"::: )  (Set (Var "U")))  "}"   "is"   ($#v4_card_3 :::"countable"::: )  )) ; 
 registrationlet "M" be   ($#m1_hidden :::"Aleph":::); 
cluster (Set   ($#k3_card_2 :::"exp"::: )   "(" (Num 2) "," "M" ")" ) ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; definitionfunc  :::"continuum":::  ->   ($#v1_finset_1 :::"infinite"::: )     ($#v1_card_1 :::"cardinal"::: )     ($#m1_hidden :::"number"::: )   equals :: TOPGEN_3:def 4 (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k1_numbers :::"REAL"::: ) )); end; 




:: deftheorem    defines :::"continuum"::: TOPGEN_3:def 4 :  (Bool (Set   ($#k3_topgen_3 :::"continuum"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ))); 
 
theorem :: TOPGEN_3:20 (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "q")) ($#k3_rcomp_1 :::".["::: ) ) where x, q "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) : (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) & (Bool (Set (Var "q")) "is"   ($#v1_rat_1 :::"rational"::: )  )  ")" )  "}"  )  ($#r1_hidden :::"="::: )  (Set   ($#k3_topgen_3 :::"continuum"::: )  )) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func "X" :::"-powers"::: "r" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) means :: TOPGEN_3:def 5 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set it  ($#k8_nat_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set "r"  ($#k1_newton :::"|^"::: )  (Set (Var "i"))))  ")" ) "or" (Bool  "("  (Bool (Bool  "not" (Set (Var "i"))  ($#r2_hidden :::"in"::: )  "X")) & (Bool (Set it  ($#k8_nat_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )); end; 






:: deftheorem    defines :::"-powers"::: TOPGEN_3:def 5 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k4_topgen_3 :::"-powers"::: )  (Set (Var "r")))) "iff" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Set (Var "b3"))  ($#k8_nat_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Set (Var "i"))))  ")" ) "or" (Bool  "("  (Bool (Bool  "not" (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool (Set (Set (Var "b3"))  ($#k8_nat_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" ))  ")" )))); 
 
theorem :: TOPGEN_3:21 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "X"))  ($#k4_topgen_3 :::"-powers"::: )  (Set (Var "r"))) "is"   ($#v1_series_1 :::"summable"::: )  ))) ; 
 









theorem :: TOPGEN_3:22 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool (Set   ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set  "(" (Set (Var "r"))  ($#k1_prepower :::"GeoSeq"::: )  ")" )  ($#k10_nat_1 :::"^\"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ))))) ; 
 
theorem :: TOPGEN_3:23 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )  ($#k1_prepower :::"GeoSeq"::: )  ")" )  ($#k10_nat_1 :::"^\"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n"))))) ; 
 
theorem :: TOPGEN_3:24 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool (Set   ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set (Var "X"))  ($#k4_topgen_3 :::"-powers"::: )  (Set (Var "r")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set (Var "r"))  ($#k1_prepower :::"GeoSeq"::: )  ")" ))))) ; 
 
theorem :: TOPGEN_3:25 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set  "(" (Set (Var "X"))  ($#k4_topgen_3 :::"-powers"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k10_nat_1 :::"^\"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: TOPGEN_3:26 (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"infinite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "(" (Set (Var "X"))  ($#k4_topgen_3 :::"-powers"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "i")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set (Var "X"))  ($#k4_topgen_3 :::"-powers"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" ))))) ; 
 
theorem :: TOPGEN_3:27 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v1_finset_1 :::"infinite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  "st" (Bool (Bool (Set   ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set (Var "X"))  ($#k4_topgen_3 :::"-powers"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_topgen_3 :::"-powers"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))) ; 
 
theorem :: TOPGEN_3:28 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v4_card_3 :::"countable"::: )  )) "holds"  (Bool (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X"))) "is"   ($#v4_card_3 :::"countable"::: )  )) ; 
 
theorem :: TOPGEN_3:29 (Bool (Set   ($#k3_topgen_3 :::"continuum"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Num 2) "," (Set  ($#k4_ordinal1 :::"omega"::: ) ) ")" )) ; 
 
theorem :: TOPGEN_3:30 (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topgen_3 :::"continuum"::: )  )) ; 
 
theorem :: TOPGEN_3:31 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topgen_3 :::"continuum"::: )  ))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set (Var "x")) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) : (Bool  "ex" (Set (Var "U")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "U"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set (Var "A")))) & (Bool (Set (Var "x"))  ($#r1_topgen_3 :::"is_local_minimum_of"::: )  (Set (Var "U")))  ")" ))  "}"  )  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topgen_3 :::"continuum"::: )  ))) ; 
 
theorem :: TOPGEN_3:32 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topgen_3 :::"continuum"::: )  ))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  (Bool  "ex" (Set (Var "q")) "being"   ($#v1_rat_1 :::"rational"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) & (Bool (Bool  "not" (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "q")) ($#k3_rcomp_1 :::".["::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set (Var "X")))))  ")" )))) ; 
 
theorem :: TOPGEN_3:33 (Bool (Set   ($#k2_waybel23 :::"weight"::: )  (Set  ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topgen_3 :::"continuum"::: )  )) ; 
 begin  definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"ClFinTop"::: "X" ->   ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) means :: TOPGEN_3:def 6 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  "X") & (Bool  "("   "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" it "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v4_pre_topc :::"closed"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_finset_1 :::"finite"::: )  ) "or" (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  "X")  ")" )  ")" )  ")" )  ")" ); end; 





:: deftheorem    defines :::"ClFinTop"::: TOPGEN_3:def 6 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_topgen_3 :::"ClFinTop"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "b2")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v4_pre_topc :::"closed"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_finset_1 :::"finite"::: )  ) "or" (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" )  ")" )  ")" )  ")" )  ")" ))); 
 
theorem :: TOPGEN_3:34 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_topgen_3 :::"ClFinTop"::: )  (Set (Var "X")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v3_pre_topc :::"open"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  )) "or" (Bool (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )  ")" ))) ; 
 
theorem :: TOPGEN_3:35 (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"infinite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ) "is"   ($#v1_finset_1 :::"infinite"::: )  ))) ; 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k5_topgen_3 :::"ClFinTop"::: )  "X") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )   ; 
end; 
theorem :: TOPGEN_3:36 (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"infinite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "U")) "," (Set (Var "V")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_topgen_3 :::"ClFinTop"::: )  (Set (Var "X")) ")" )  "holds" (Bool (Set (Var "U"))  ($#r2_subset_1 :::"meets"::: )  (Set (Var "V"))))) ; 
 begin  definitionlet "X", "x0" be    ($#m1_hidden :::"set"::: )  ; func "x0" :::"-PointClTop"::: "X" ->   ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) means :: TOPGEN_3:def 7 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  "X") & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" it "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k14_funcop_1 :::"IFEQ"::: )   "(" (Set (Var "A")) "," (Set  ($#k11_arytm_3 :::"{}"::: ) ) "," (Set (Var "A")) "," (Set  "(" (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set  ($#k1_tarski :::"{"::: ) "x0" ($#k1_tarski :::"}"::: ) )  ($#k3_xboole_0 :::"/\"::: )  "X" ")" ) ")" ) ")" ))  ")" )  ")" ); end; 






:: deftheorem    defines :::"-PointClTop"::: TOPGEN_3:def 7 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "x0")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x0"))  ($#k6_topgen_3 :::"-PointClTop"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "b3")) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k14_funcop_1 :::"IFEQ"::: )   "(" (Set (Var "A")) "," (Set  ($#k11_arytm_3 :::"{}"::: ) ) "," (Set (Var "A")) "," (Set  "(" (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X")) ")" ) ")" ) ")" ))  ")" )  ")" )  ")" ))); 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "x0" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "x0"  ($#k6_topgen_3 :::"-PointClTop"::: )  "X") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )   ; 
end; 
theorem :: TOPGEN_3:37 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "x0"))  ($#k6_topgen_3 :::"-PointClTop"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x0")) ($#k6_domain_1 :::"}"::: ) )))))) ; 
 
theorem :: TOPGEN_3:38 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "x0"))  ($#k6_topgen_3 :::"-PointClTop"::: )  (Set (Var "X")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ) "iff" (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )))) ; 
 
theorem :: TOPGEN_3:39 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "being"   ($#v1_subset_1 :::"proper"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "x0"))  ($#k6_topgen_3 :::"-PointClTop"::: )  (Set (Var "X")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v3_pre_topc :::"open"::: )  ) "iff" (Bool (Bool  "not" (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))  ")" )))) ; 
 
theorem :: TOPGEN_3:40 (Bool  "for" (Set (Var "X")) "," (Set (Var "x0")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "is"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "x0"))  ($#k6_topgen_3 :::"-PointClTop"::: )  (Set (Var "X")) ")" )) "iff" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x0")))  ")" )) ; 
 
theorem :: TOPGEN_3:41 (Bool  "for" (Set (Var "X")) "," (Set (Var "x0")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) )  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "x0"))  ($#k6_topgen_3 :::"-PointClTop"::: )  (Set (Var "X")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x0")))  ")" )  ")" )) ; 
 begin  definitionlet "X", "X0" be    ($#m1_hidden :::"set"::: )  ; func "X0" :::"-DiscreteTop"::: "X" ->   ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) means :: TOPGEN_3:def 8 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  "X") & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" it "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set (Var "A")) "," "X" "," (Set (Var "A")) "," (Set  "(" (Set (Var "A"))  ($#k8_subset_1 :::"/\"::: )  "X0" ")" ) ")" ))  ")" )  ")" ); end; 






:: deftheorem    defines :::"-DiscreteTop"::: TOPGEN_3:def 8 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "X0")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X0"))  ($#k7_topgen_3 :::"-DiscreteTop"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "b3")) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_funcop_1 :::"IFEQ"::: )   "(" (Set (Var "A")) "," (Set (Var "X")) "," (Set (Var "A")) "," (Set  "(" (Set (Var "A"))  ($#k8_subset_1 :::"/\"::: )  (Set (Var "X0")) ")" ) ")" ))  ")" )  ")" )  ")" ))); 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "X0" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "X0"  ($#k7_topgen_3 :::"-DiscreteTop"::: )  "X") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )   ; 
end; 
theorem :: TOPGEN_3:42 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X0")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v1_subset_1 :::"proper"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "X0"))  ($#k7_topgen_3 :::"-DiscreteTop"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k8_subset_1 :::"/\"::: )  (Set (Var "X0"))))))) ; 
 
theorem :: TOPGEN_3:43 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X0")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v1_subset_1 :::"proper"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "X0"))  ($#k7_topgen_3 :::"-DiscreteTop"::: )  (Set (Var "X")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v3_pre_topc :::"open"::: )  ) "iff" (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "X0")))  ")" )))) ; 
 
theorem :: TOPGEN_3:44 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set  "(" (Set (Var "X0"))  ($#k7_topgen_3 :::"-DiscreteTop"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X0")) ")" ))))) ; 
 
theorem :: TOPGEN_3:45 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_tex_1 :::"ADTS"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k11_arytm_3 :::"{}"::: ) )  ($#k7_topgen_3 :::"-DiscreteTop"::: )  (Set (Var "X"))))) ; 
 
theorem :: TOPGEN_3:46 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_compts_1 :::"1TopSp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k7_topgen_3 :::"-DiscreteTop"::: )  (Set (Var "X"))))) ;