:: deftheorem defines open-domains-family TDLAT_2:def 4 :
for T being non empty TopSpace
for IT being Subset-Family of T holds
( IT is open-domains-family iff for A being Subset of T st A in IT holds
A is open_condensed );