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

proof

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

end;

Lang (w,S) c= Lang (w,(S \/ T)) by Th48, XBOOLE_1:7;
hence Lang (w,S) = Lang (w,(S \/ T)) by A2, XBOOLE_0:def 10; :: according to REWRITE2:def 9 :: thesis: verum