FDL > PVS > Prelude > sets > choose : const-decl

choose((p:(nonempty?) )): (p) = epsilon(p);