let E be set ; :: thesis: for S being semi-Thue-system of E
for w being Element of E ^omega holds Lang w,S = Lang w,(S \/ (id (E ^omega )))
let S be semi-Thue-system of E; :: thesis: for w being Element of E ^omega holds Lang w,S = Lang w,(S \/ (id (E ^omega )))
let w be Element of E ^omega ; :: thesis: Lang w,S = Lang w,(S \/ (id (E ^omega )))
A1: Lang w,(S \/ (id (E ^omega ))) c= Lang w,S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Lang w,(S \/ (id (E ^omega ))) or x in Lang w,S )
assume A2: x in Lang w,(S \/ (id (E ^omega ))) ; :: thesis: x in Lang w,S
then reconsider s = x as Element of E ^omega ;
w ==>* s,S \/ (id (E ^omega )) by A2, Th46;
then w ==>* s,S by Th41;
hence x in Lang w,S ; :: thesis: verum

end;

Lang w,S c= Lang w,(S \/ (id (E ^omega ))) by Th48, XBOOLE_1:7;
hence Lang w,S = Lang w,(S \/ (id (E ^omega ))) by A1, XBOOLE_0:def 10; :: thesis: verum