theorem Th43: :: REWRITE2:43

for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega st s ==>* t, ==>.-relation S holds
s ==>* t,S by Th31;