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

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