:: deftheorem Def7 defines COMPLEMENT SETFAM_1:def 7 :
for D being set
for F, b₃ being Subset-Family of D holds
( b₃ = COMPLEMENT F iff for P being Subset of D holds
( P in b₃ iff P ` in F ) );