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

( 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