theorem :: REWRITE2:55

for E being set
for S being semi-Thue-system of E
for w being Element of E ^omega holds S,S \/ (id (E ^omega)) are_equivalent_wrt w by Th49;