theorem Th92: :: REWRITE3:92

for x, y being object
for E being non empty set
for e being Element of E
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS holds
x,<%e%> ==>. y, <%> E,TS