let x1, x2, y1, y2 be object ; :: thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
==>.-relation TS reduces [x1,x2],[y1,y2]
let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
==>.-relation TS reduces [x1,x2],[y1,y2]
let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
==>.-relation TS reduces [x1,x2],[y1,y2]
let TS be non empty transition-system over F; :: thesis: ( x1,x2 ==>. y1,y2,TS implies ==>.-relation TS reduces [x1,x2],[y1,y2] )
assume x1,x2 ==>. y1,y2,TS ; :: thesis: ==>.-relation TS reduces [x1,x2],[y1,y2]
then [[x1,x2],[y1,y2]] in ==>.-relation TS by Def4;
hence ==>.-relation TS reduces [x1,x2],[y1,y2] by REWRITE1:15; :: thesis: verum