:: deftheorem defines discrete TEX_2:def 4 :
for Y being TopStruct
for A being Subset of Y holds
( A is discrete iff for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D ) );