theorem Th7: :: YELLOW_8:7

for X being 1-sorted
for F being Subset-Family of X holds union (COMPLEMENT F) = (Intersect F) `