:: deftheorem defines ==>. REWRITE3:def 3 :
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F
for x1, x2, y1, y2 being object holds
( x1,x2 ==>. y1,y2,TS iff ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) );