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 & S c= U & U c= T holds
( S,U are_equivalent_wrt w & U,T are_equivalent_wrt w )