let D be set ; :: thesis: for F being Subset-Family of D st F <> {} holds
COMPLEMENT F <> {}
let F be Subset-Family of D; :: thesis: ( F <> {} implies COMPLEMENT F <> {} )
set X = the Element of F;
assume A1: F <> {} ; :: thesis: COMPLEMENT F <> {}
then reconsider X = the Element of F as Subset of D by TARSKI:def 3;
(X `) ` = X ;
hence COMPLEMENT F <> {} by A1, Def7; :: thesis: verum