theorem :: REWRITE3:97

for x, y, z being object
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
x,y ==>* z,TS by Th84;