let T be set ; :: thesis: for F being Subset-Family of T st F <> {} holds
meet (COMPLEMENT F) = (union F) `
let F be Subset-Family of T; :: thesis: ( F <> {} implies meet (COMPLEMENT F) = (union F) ` )
assume F <> {} ; :: thesis: meet (COMPLEMENT F) = (union F) `
then meet (COMPLEMENT F) = ([#] T) \ (union F) by SETFAM_1:33;
hence meet (COMPLEMENT F) = (union F) ` ; :: thesis: verum