let T be set ; :: thesis: for F being Subset-Family of T holds
( F is countable iff COMPLEMENT F is countable )
let F be Subset-Family of T; :: thesis: ( F is countable iff COMPLEMENT F is countable )
F, COMPLEMENT F are_equipotent by YELLOW_8:3;
hence ( F is countable iff COMPLEMENT F is countable ) by YELLOW_8:4; :: thesis: verum