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