:: deftheorem Def2 defines Choice ORDERS_1:def 2 :
for I being set
for M, b₃ being ManySortedSet of I holds
( b₃ is Choice of M iff for x being object st x in I holds
b₃ . x = the Element of M . x );