let E be set ; :: thesis: for S being semi-Thue-system of E
for s being Element of E ^omega holds s ==>* s,S
let S be semi-Thue-system of E; :: thesis: for s being Element of E ^omega holds s ==>* s,S
let s be Element of E ^omega ; :: thesis: s ==>* s,S
==>.-relation S reduces s,s by REWRITE1:12;
hence s ==>* s,S by Def7; :: thesis: verum