let T be 1-sorted ; :: thesis: for F being Subset-Family of T holds
( COMPLEMENT F is finite iff F is finite )
let F be Subset-Family of T; :: thesis: ( COMPLEMENT F is finite iff F is finite )
thus ( COMPLEMENT F is finite implies F is finite ) by Lm1; :: thesis: ( F is finite implies COMPLEMENT F is finite )
assume F is finite ; :: thesis: COMPLEMENT F is finite
then COMPLEMENT (COMPLEMENT F) is finite ;
hence COMPLEMENT F is finite by Lm1; :: thesis: verum