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

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