for E being set
for S being semi-Thue-system of E
for s being Element of E ^omega st s ==>. s,S holds
ex v, w, s1 being Element of E ^omega st
( s = (v ^ s1) ^ w & s1 -->. s1,S )