let E be set ; :: thesis: for S, T being semi-Thue-system of E
for w being Element of E ^omega st S,T are_equivalent_wrt w holds
T,S are_equivalent_wrt w
let S, T be semi-Thue-system of E; :: thesis: for w being Element of E ^omega st S,T are_equivalent_wrt w holds
T,S are_equivalent_wrt w
let w be Element of E ^omega ; :: thesis: ( S,T are_equivalent_wrt w implies T,S are_equivalent_wrt w )
assume Lang (w,S) = Lang (w,T) ; :: according to REWRITE2:def 9 :: thesis: T,S are_equivalent_wrt w
hence T,S are_equivalent_wrt w by Def9; :: thesis: verum