Description: Define the limit ordinal predicate, which is true for a nonempty ordinal
that is not a successor (i.e. that is the union of itself). Our
definition combines the definition of Lim of BellMachover p. 471 and
Exercise 1 of TakeutiZaring p. 42. See dflim2 , dflim3 , and dflim4
for alternate definitions. (Contributed by NM, 22-Apr-1994)