for X being TopStruct
for F being Subset-Family of X holds
( F is open iff F c= the topology of X )