:: deftheorem defines Lang REWRITE2:def 8 :
for E being set
for S being semi-Thue-system of E
for w being Element of E ^omega holds Lang (w,S) = { s where s is Element of E ^omega : w ==>* s,S } ;