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)

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

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

Lang (w,S) c= Lang (w,(==>.-relation S))
by Th22, Th48;
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;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

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