theorem :: TOPS_2:5

for T being set
for F being Subset-Family of T holds
( F <> {} iff COMPLEMENT F <> {} )