:: deftheorem defines ==>. REWRITE2:def 5 :
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 ex v, w, s1, t1 being Element of E ^omega st
( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w & s1 -->. t1,S ) );