Description: Define the transitive predecessors of a class X under a relation
R in a class A . This class can be thought of as the "smallest"
class containing all elements of A that are linked to X by an
R -chain (see trpredtr and trpredmintr ). Definition based on
Theorem 8.4 of Don Monk's notes for Advanced Set Theory, which can be
found at https://euclid.colorado.edu/~monkd/setth.pdf . (Contributed by Scott Fenton, 2-Feb-2011)