theorem Th31: :: REWRITE3:31

for x, y 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] in ==>.-relation TS holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( x = [s,v] & y = [t,w] )