Description: Define the cardinal number function. The cardinal number of a set is
the least ordinal number equinumerous to it. In other words, it is the
"size" of the set. Definition of Enderton p. 197. See cardval for
its value and cardval2 for a simpler version of its value. The
principal theorem relating cardinality to equinumerosity is carden .
Our notation is from Enderton. Other textbooks often use a double bar
over the set to express this function. (Contributed by NM, 21-Oct-2003)