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