:: deftheorem Def2 defines SgmX PRE_POLY:def 2 :
for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
for b₄ being FinSequence of X holds
( b₄ = SgmX (R,A) iff ( rng b₄ = A & ( for n, m being Nat st n in dom b₄ & m in dom b₄ & n < m holds
( b₄ /. n <> b₄ /. m & [(b₄ /. n),(b₄ /. m)] in R ) ) ) );