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 set ; :: 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