theorem Th32: :: SETFAM_1:32

for D being set
for F being Subset-Family of D st F <> {} holds
COMPLEMENT F <> {}