theorem :: SETFAM_1:35

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