:: deftheorem defines with_countable_Cover SRINGS_1:def 4 :
for X being set
for S being Subset-Family of X holds
( S is with_countable_Cover iff ex XX being countable Subset of S st XX is Cover of X );