Description: If Y belongs to the R -sequence beginning with Z , then
every result of an application of the procedure R to Y belongs
to the R -sequence beginning with Z or precedes Z in the
R -sequence. Proposition 111 of Frege1879 p. 75. (Contributed by RP, 7-Jul-2020)(Revised by RP, 8-Jul-2020)(Proof modification is discouraged.)