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 s ==>. t,S ; :: thesis: S,S \/ {[s,t]} are_equivalent_wrt w

then [s,t] in ==>.-relation S by Def6;

then {[s,t]} c= ==>.-relation S by ZFMISC_1:31;

then A1: S \/ {[s,t]} c= S \/ (==>.-relation S) by XBOOLE_1:9;

( S,S \/ (==>.-relation S) are_equivalent_wrt w & S c= S \/ {[s,t]} ) by Th57, Th60, XBOOLE_1:7;

hence S,S \/ {[s,t]} are_equivalent_wrt w by A1, Th56; :: thesis: verum

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 s ==>. t,S ; :: thesis: S,S \/ {[s,t]} are_equivalent_wrt w

then [s,t] in ==>.-relation S by Def6;

then {[s,t]} c= ==>.-relation S by ZFMISC_1:31;

then A1: S \/ {[s,t]} c= S \/ (==>.-relation S) by XBOOLE_1:9;

( S,S \/ (==>.-relation S) are_equivalent_wrt w & S c= S \/ {[s,t]} ) by Th57, Th60, XBOOLE_1:7;

hence S,S \/ {[s,t]} are_equivalent_wrt w by A1, Th56; :: thesis: verum