theorem Th83:
for
x1,
x2,
y1,
y2,
z1,
z2 being
object 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 &
y1,
y2 ==>* z1,
z2,
TS holds
x1,
x2 ==>* z1,
z2,
TS by REWRITE1:16;