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