theorem Th16: :: TOPGEN_4:16

for T being set
for F, G being Subset-Family of T st F c= G & G is compl-closed holds
COMPLEMENT F c= G