Description: If Z is a result of an application of the procedure R to an
object Y that follows X in the R -sequence and if every
result of an application of the procedure R to X has a
property A that is hereditary in the R -sequence, then Z
has property A . Proposition 87 of Frege1879 p. 66.
(Contributed by RP, 1-Jul-2020)(Revised by RP, 7-Jul-2020)(Proof modification is discouraged.)