theorem Th31: :: REWRITE2:31

for E being set
for S being semi-Thue-system of E holds ==>.-relation (==>.-relation S) = ==>.-relation S