let x, y, z be set ; :: thesis: for E being non empty set
for F being Subset of (E ^omega )
for TS being non empty transition-system of F st x,y -->. z,TS holds
x,y ==>* z, <%> E,TS
let E be non empty set ; :: thesis: for F being Subset of (E ^omega )
for TS being non empty transition-system of F st x,y -->. z,TS holds
x,y ==>* z, <%> E,TS
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F st x,y -->. z,TS holds
x,y ==>* z, <%> E,TS
let TS be non empty transition-system of F; :: thesis: ( x,y -->. z,TS implies x,y ==>* z, <%> E,TS )
assume x,y -->. z,TS ; :: thesis: x,y ==>* z, <%> E,TS
then ==>.-relation TS reduces [x,y],[z,(<%> E)] by ThRed81;
hence x,y ==>* z, <%> E,TS by DefTran; :: thesis: verum