Description: If F is a function, A is the successor of X , and B
follows X in the transitive closure of F , then (for distinct
A and B ) either A follows B or B follows A in
the transitive closure of F . Similar to Proposition 126 of
Frege1879 p. 81. Compare with frege126 . (Contributed by RP, 16-Jul-2020)