:: deftheorem Def1 defines discrete NAGATA_1:def 1 :
for T being TopSpace
for F being Subset-Family of T holds
( F is discrete iff for p being Point of T ex O being open Subset of T st
( p in O & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds
A = B ) ) );