let T be set ; :: thesis: for A being SetSequence of T holds rng A is non empty countable Subset-Family of T

let A be SetSequence of T; :: thesis: rng A is non empty countable Subset-Family of T

A . 1 in rng A by FUNCT_2:4;

then reconsider AA = rng A as non empty Subset-Family of T ;

( card (rng A) c= card (dom A) & dom A is countable ) by CARD_2:61, FUNCT_2:def 1;

then AA is countable by WAYBEL12:1;

hence rng A is non empty countable Subset-Family of T ; :: thesis: verum

let A be SetSequence of T; :: thesis: rng A is non empty countable Subset-Family of T

A . 1 in rng A by FUNCT_2:4;

then reconsider AA = rng A as non empty Subset-Family of T ;

( card (rng A) c= card (dom A) & dom A is countable ) by CARD_2:61, FUNCT_2:def 1;

then AA is countable by WAYBEL12:1;

hence rng A is non empty countable Subset-Family of T ; :: thesis: verum