Definition 1.8.2.3.  Let κ be a cardinal number. We define
(κ)
by:
(|K|) := K  (K is a set)
We write “let a ∈ κ” for “let a ∈ (κ).”
Remarks.

This definition retrieves a representative set from a cardinal number.