let E be set ; :: thesis: 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
let S, T, U be semi-Thue-system of E; :: thesis: 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
let w be Element of E ^omega ; :: thesis: ( S,T are_equivalent_wrt w & T,U are_equivalent_wrt w implies S,U are_equivalent_wrt w )
assume ( Lang w,S = Lang w,T & Lang w,T = Lang w,U ) ; :: according to REWRITE2:def 9 :: thesis: S,U are_equivalent_wrt w
hence S,U are_equivalent_wrt w by Def9; :: thesis: verum