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)

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

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

Lang (w,S) c= Lang (w,(S \/ (id (E ^omega))))
by Th48, XBOOLE_1:7;
let x be object ; :: 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;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

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