theorem Th79: :: REWRITE3:79

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) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds
[[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS