theorem Th28: :: FSM_3:28

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 p, q being Element of TS st p,u ^ v ==>* q,TS holds
ex r being Element of TS st
( p,u ==>* r,TS & r,v ==>* q,TS )