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