let x, y 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 holds x,y ==>* x,y,TS
let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system of F holds x,y ==>* x,y,TS
let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system of F holds x,y ==>* x,y,TS
let TS be non empty transition-system of F; :: thesis: x,y ==>* x,y,TS
==>.-relation TS reduces [x,y],[x,y] by REWRITE1:12;
hence x,y ==>* x,y,TS by Def6; :: thesis: verum