:: deftheorem Def1 defines countable MSAFREE4:def 1 :
for I being set
for A being ManySortedSet of I holds
( A is countable iff for x being set st x in I holds
A . x is countable );