:: deftheorem Def1 defines Choice ORDERS_1:def 1 :
for f, b₂ being Function holds
( b₂ is Choice of f iff ( dom b₂ = dom f & ( for x being object st x in dom f holds
b₂ . x = the Element of f . x ) ) );