theorem :: TOPGEN_4:15
for T being set
for F being Subset-Family of T st F is compl-closed holds
F = COMPLEMENT F