for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds
len P = 1