let E be set ; :: thesis: for S being semi-Thue-system of E
for w being Element of E ^omega holds S, ==>.-relation S are_equivalent_wrt w
let S be semi-Thue-system of E; :: thesis: for w being Element of E ^omega holds S, ==>.-relation S are_equivalent_wrt w
let w be Element of E ^omega ; :: thesis: S, ==>.-relation S are_equivalent_wrt w
A1: Lang (w,(==>.-relation S)) c= Lang (w,S)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lang (w,(==>.-relation S)) or x in Lang (w,S) )
assume A2: x in Lang (w,(==>.-relation S)) ; :: thesis: x in Lang (w,S)
reconsider s = x as Element of E ^omega by A2;
w ==>* s, ==>.-relation S by A2, Th46;
then w ==>* s,S by Th43;
hence x in Lang (w,S) ; :: thesis: verum

end;

Lang (w,S) c= Lang (w,(==>.-relation S)) by Th22, Th48;
hence Lang (w,S) = Lang (w,(==>.-relation S)) by A1, XBOOLE_0:def 10; :: according to REWRITE2:def 9 :: thesis: verum