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