:: deftheorem Def2 defines RedSequence REWRITE1:def 2 :
for R being Relation
for b₂ being FinSequence holds
( b₂ is RedSequence of R iff ( len b₂ > 0 & ( for i being Nat st i in dom b₂ & i + 1 in dom b₂ holds
[(b₂ . i),(b₂ . (i + 1))] in R ) ) );