:: deftheorem Def6 defines ==>.-relation REWRITE2:def 6 :
for E being set
for S being semi-Thue-system of E
for b₃ being Relation of (E ^omega) holds
( b₃ = ==>.-relation S iff for s, t being Element of E ^omega holds
( [s,t] in b₃ iff s ==>. t,S ) );