let E be set ; :: thesis: for S being semi-Thue-system of E
for w being Element of E ^omega holds w in Lang w,S
let S be semi-Thue-system of E; :: thesis: for w being Element of E ^omega holds w in Lang w,S
let w be Element of E ^omega ; :: thesis: w in Lang w,S
w ==>* w,S by Th32;
hence w in Lang w,S ; :: thesis: verum