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:46; :: thesis: ( COMPLEMENT F <> {} implies F <> {} )
assume COMPLEMENT F <> {} ; :: thesis: F <> {}
then COMPLEMENT (COMPLEMENT F) <> {} by SETFAM_1:46;
hence F <> {} ; :: thesis: verum