:: deftheorem Def11 defines order MMLQUER2:def 11 :
for X being set
for R being connected Order of X
for S being finite Subset of X
for b₄ being XFinSequence of X holds
( b₄ = order (S,R) iff ( rng b₄ = S & b₄ is one-to-one & ( for i, j being Nat st i in dom b₄ & j in dom b₄ holds
( i <= j iff b₄ . i,b₄ . j in R ) ) ) );