theorem Th37: :: REWRITE3:37

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)]] in ==>.-relation TS )