theorem Th64: :: TOPS_2:64

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