let x 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, <%> E ==>* x,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, <%> E ==>* x,TS
let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system of F holds x, <%> E ==>* x,TS
let TS be non empty transition-system of F; :: thesis: x, <%> E ==>* x,TS
x, <%> E ==>* x, <%> E,TS by Th82;
hence x, <%> E ==>* x,TS by Def7; :: thesis: verum