theorem Th59: :: REWRITE2:59

for E being set
for S, T being semi-Thue-system of E
for s, w being Element of E ^omega st S,T are_equivalent_wrt w & w ==>* s,S \/ T holds
w ==>* s,S by Th58;