theorem Th8: :: TOPS_2:8

for T being 1-sorted
for F being Subset-Family of T holds
( COMPLEMENT F is finite iff F is finite )