theorem :: SETFAM_1:33

for D being set
for F being Subset-Family of D st F <> {} holds
([#] D) \ (union F) = meet (COMPLEMENT F)