theorem :: BAGORD_2:60

for I being set
for R being asymmetric Relation of I
for p, q, r being b₁ -valued FinSequence holds
( [p,q] in LexOrder (I,R) iff [(r ^ p),(r ^ q)] in LexOrder (I,R) )