theorem Th57: :: REWRITE2:57

for E being set
for S being semi-Thue-system of E
for w being Element of E ^omega holds S, ==>.-relation S are_equivalent_wrt w