for E being non empty set
for u, v being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds
ex l being Nat st
( l in dom R & (R . l) `2 = v )