theorem Th35: :: REWRITE2:35

for E being set
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 by REWRITE1:16;