for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( P . k = [s,v] & P . (k + 1) = [t,w] )