:: deftheorem Def7 defines -PointClTop TOPGEN_3:def 7 :
for X, x0 being set
for b₃ being strict TopSpace holds
( b₃ = x0 -PointClTop X iff ( the carrier of b₃ = X & ( for A being Subset of b₃ holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) ) );