:: deftheorem defines open TOPS_2:def 1 :
for T being TopStruct
for F being Subset-Family of T holds
( F is open iff for P being Subset of T st P in F holds
P is open );