:: deftheorem defines down CARD_3:def 17 :
for I being set
for f being non-empty ManySortedSet of I
for M being b₂ -compatible ManySortedSet of I holds down M = M;