theorem Th12: :: FSM_3:12

for x, y being set
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 x,<%e%> ==>* y, <%> E, _bool TS holds
x,<%e%> ==>. y, <%> E, _bool TS