|Description: Define class difference,
also called relative complement. Definition
5.12 of [TakeutiZaring] p. 20.
Contrast this operation with union
(df-un 3041) and intersection (df-in 3043).
Several notations are used in the literature; we chose the
convention used in Definition 5.3 of [Eisenberg] p. 67 instead of the
more common minus sign to reserve the latter for later use in, e.g.,
arithmetic. We will use the terminology " excludes " to
mean . We will use " is removed from " to mean
i.e. the removal of an element or equivalently the
exclusion of a singleton. (Contributed by NM,