let E be set ; :: thesis: for S being semi-Thue-system of E
for w being Element of E ^omega holds S,S are_equivalent_wrt w
let S be semi-Thue-system of E; :: thesis: for w being Element of E ^omega holds S,S are_equivalent_wrt w
let w be Element of E ^omega ; :: thesis: S,S are_equivalent_wrt w
thus Lang (w,S) = Lang (w,S) ; :: according to REWRITE2:def 9 :: thesis: verum