theorem Th40: :: REWRITE2:40

for E being set
for S, T being semi-Thue-system of E
for s, t being Element of E ^omega st S c= T & s ==>* t,S holds
s ==>* t,T by Th26, REWRITE1:22;