theorem :: SETFAM_1:40

for X being set
for F being Subset-Family of X st F = {X} holds
COMPLEMENT F = {{}}