:: deftheorem Def8 defines -DiscreteTop TOPGEN_3:def 8 :
for X, X0 being set
for b₃ being strict TopSpace holds
( b₃ = X0 -DiscreteTop X iff ( the carrier of b₃ = X & ( for A being Subset of b₃ holds Int A = IFEQ (A,X,A,(A /\ X0)) ) ) );