theorem Th9: :: TOPS_2:9

for T being TopStruct
for F being Subset-Family of T holds
( F is closed iff COMPLEMENT F is open )