The VALUE-CARDINALITY of a binary-relation with respect to a given domain instance is the number of range-elements to which the relation maps the domain-element. For a function (single-valued relation), the VALUE-CARDINALITY is 1 on all domain instances for which the function is defined. It is 0 for those instances outside the exact domain of the function.VALUE-CARDINALITY may be used within the definition of a class to specify a slot cardinality if its first argument is the class's instance variable.
(Nth-Domain Value-Cardinality 3 Nonnegative-Integer)
(Nth-Domain Value-Cardinality 2 Binary-Relation)
(=> (Value-Cardinality ?Instance ?Binary-Relation ?N)
(= ?N
(Cardinality (Setofall ?Y
(Holds ?Binary-Relation ?Instance ?Y)))))