theorem Th23: :: REWRITE3:23

for x, y, z being object
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F holds
( x,y -->. z,TS iff x,y ==>. z, <%> E,TS )