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