let E be set ; :: thesis: for S being semi-Thue-system of E
for w being Element of E ^omega holds S,S \/ (id (E ^omega )) are_equivalent_wrt w
let S be semi-Thue-system of E; :: thesis: for w being Element of E ^omega holds S,S \/ (id (E ^omega )) are_equivalent_wrt w
let w be Element of E ^omega ; :: thesis: S,S \/ (id (E ^omega )) are_equivalent_wrt w
Lang w,S = Lang w,(S \/ (id (E ^omega ))) by Th49;
hence S,S \/ (id (E ^omega )) are_equivalent_wrt w by Def9; :: thesis: verum