for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega st S is Thue-system of E & s ==>. t,S holds
t ==>. s,S by Th16;