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