:: deftheorem defines ChoiceOn HILBERT4:def 1 :
for X being set holds ChoiceOn X = { [x, the Element of x] where x is Element of X \ {{}} : x in X \ {{}} } ;