theorem Th57: :: REWRITE3:57

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 holds
( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS )