let x1, x2, 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 st x1,x2 ==>. y, <%> E,TS holds
x1,x2 ==>* 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 st x1,x2 ==>. y, <%> E,TS holds
x1,x2 ==>* y,TS
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F st x1,x2 ==>. y, <%> E,TS holds
x1,x2 ==>* y,TS
let TS be non empty transition-system of F; :: thesis: ( x1,x2 ==>. y, <%> E,TS implies x1,x2 ==>* y,TS )
assume x1,x2 ==>. y, <%> E,TS ; :: thesis: x1,x2 ==>* y,TS
then x1,x2 ==>* y, <%> E,TS by ThTran40;
hence x1,x2 ==>* y,TS by DefAcc; :: thesis: verum