theorem :: SETFAM_1:34

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