theorem Lem13: :: BAGORD_2:10

for p, q, r being FinSequence holds
( r ^ p c< r ^ q iff p c< q )