theorem :: REWRITE2:54

for E being set
for S, T, U being semi-Thue-system of E
for w being Element of E ^omega st S,T are_equivalent_wrt w & T,U are_equivalent_wrt w holds
S,U are_equivalent_wrt w ;