:: deftheorem defines dense WAYBEL12:def 2 :
for T being TopStruct
for F being Subset-Family of T holds
( F is dense iff for X being Subset of T st X in F holds
X is dense );