A choice function on a set of inhabited sets is a function which “chooses” an element from each set , #m/def/set i.e.
Within , a choice function cannot be guaranteed unless an explicit rule can be given for choosing elements, e.g. the smallest element of well ordered sets.
To guarantee the existence of a choice function for an arbitrary set of inhabited sets, the Axiom of Choice is required.