**Defined in theory: Kif-sets****Source code: kif-sets.lisp**

**Documentation:**There is a set that associates every bounded set with a distinguished element of that set. In effect, it {it chooses} an element from every bounded set.

**Instance-Of:**Sentence**Defining-Axiom:**'(Exists (?S) (And (Set ?S) (Forall (?X) (=> (Member ?X ?S) (Double ?X))) (Forall (?X ?Y ?Z) (=> (And (Member (Listof ?X ?Y) ?S) (Member (Listof ?X ?Z) ?S)) (= ?Y ?Z))) (Forall (?U) (=> (And (Bounded ?U) (Not (Empty ?U))) (Exists (?V) (And (Member ?V ?U) (Member (Listof ?U ?V) ?S)))))))

**Source:**KIF Version 3.0 Specification