theorem :: BAGORD_2:60
for I being set
for R being asymmetric Relation of I
for p, q, r being b1 -valued FinSequence holds
( [p,q] in LexOrder (I,R) iff [(r ^ p),(r ^ q)] in LexOrder (I,R) )