theorem Th3: :: YELLOW_8:3

for X being set
for F being Subset-Family of X holds F, COMPLEMENT F are_equipotent