:: deftheorem defines ==>* REWRITE2:def 7 :
for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega holds
( s ==>* t,S iff ==>.-relation S reduces s,t );