let E be set ; :: thesis: for S being semi-Thue-system of E
for s, t, w being Element of E ^omega st s ==>* t,S holds
S,S \/ {[s,t]} are_equivalent_wrt w
let S be semi-Thue-system of E; :: thesis: for s, t, w being Element of E ^omega st s ==>* t,S holds
S,S \/ {[s,t]} are_equivalent_wrt w
let s, t, w be Element of E ^omega ; :: thesis: ( s ==>* t,S implies S,S \/ {[s,t]} are_equivalent_wrt w )
assume A1: s ==>* t,S ; :: thesis: S,S \/ {[s,t]} are_equivalent_wrt w
A2: Lang w,(S \/ {[s,t]}) c= Lang w,S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Lang w,(S \/ {[s,t]}) or x in Lang w,S )
assume A3: x in Lang w,(S \/ {[s,t]}) ; :: thesis: x in Lang w,S
reconsider u = x as Element of E ^omega by A3;
w ==>* u,S \/ {[s,t]} by A3, Th46;
then w ==>* u,S by A1, Th45;
hence x in Lang w,S ; :: thesis: verum

end;

Lang w,S c= Lang w,(S \/ {[s,t]}) by Th48, XBOOLE_1:7;
hence Lang w,S = Lang w,(S \/ {[s,t]}) by A2, XBOOLE_0:def 10; :: according to REWRITE2:def 9 :: thesis: verum