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