let E be set ; :: thesis: for S being semi-Thue-system of E
for s, t, u being Element of E ^omega st s ==>* t,S & t ==>* u,S holds
s ==>* u,S
let S be semi-Thue-system of E; :: thesis: for s, t, u being Element of E ^omega st s ==>* t,S & t ==>* u,S holds
s ==>* u,S
let s, t, u be Element of E ^omega ; :: thesis: ( s ==>* t,S & t ==>* u,S implies s ==>* u,S )
assume ( s ==>* t,S & t ==>* u,S ) ; :: thesis: s ==>* u,S
then ( ==>.-relation S reduces s,t & ==>.-relation S reduces t,u ) by Def7;
then ==>.-relation S reduces s,u by REWRITE1:17;
hence s ==>* u,S by Def7; :: thesis: verum