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,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,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,TS
let TS be non empty transition-system of F; :: thesis: ( x,y -->. z,TS implies x,y ==>* z,TS )
assume x,y -->. z,TS ; :: thesis: x,y ==>* z,TS
then x,y ==>* z, <%> E,TS by Th84;
hence x,y ==>* z,TS by Def7; :: thesis: verum