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