:: deftheorem defines are_equivalent_wrt REWRITE2:def 9 :
for E being set
for S, T being semi-Thue-system of E
for w being Element of E ^omega holds
( S,T are_equivalent_wrt w iff Lang (w,S) = Lang (w,T) );