:: deftheorem LO defines LexOrder BAGORD_2:def 14 :
for I being set
for R being Relation of I,I
for b₃ being Relation of (I *) holds
( b₃ = LexOrder (I,R) iff for p, q being b₁ -valued FinSequence holds
( [p,q] in b₃ iff ( p c< q or ex k being Nat st
( k in dom p & k in dom q & [(p . k),(q . k)] in R & ( for n being Nat st 1 <= n & n < k holds
p . n = q . n ) ) ) ) );