let T be set ; :: thesis: for F being Subset-Family of T holds
( F <> {} iff COMPLEMENT F <> {} )
let F be Subset-Family of T; :: thesis: ( F <> {} iff COMPLEMENT F <> {} )
thus ( F <> {} implies COMPLEMENT F <> {} ) by SETFAM_1:32; :: thesis: ( COMPLEMENT F <> {} implies F <> {} )
assume COMPLEMENT F <> {} ; :: thesis: F <> {}
then COMPLEMENT (COMPLEMENT F) <> {} by SETFAM_1:32;
hence F <> {} ; :: thesis: verum