for X being 1-sorted
for F being Subset-Family of X
for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )