let E be set ; :: thesis: for S, T being semi-Thue-system of E

for s, t being Element of E ^omega st S c= T & s ==>. t,S holds

s ==>. t,T

let S, T be semi-Thue-system of E; :: thesis: for s, t being Element of E ^omega st S c= T & s ==>. t,S holds

s ==>. t,T

let s, t be Element of E ^omega ; :: thesis: ( S c= T & s ==>. t,S implies s ==>. t,T )

assume that

A1: S c= T and

A2: s ==>. t,S ; :: thesis: s ==>. t,T

consider v, w, s1, t1 being Element of E ^omega such that

A3: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w ) and

A4: s1 -->. t1,S by A2;

s1 -->. t1,T by A1, A4;

hence s ==>. t,T by A3; :: thesis: verum

for s, t being Element of E ^omega st S c= T & s ==>. t,S holds

s ==>. t,T

let S, T be semi-Thue-system of E; :: thesis: for s, t being Element of E ^omega st S c= T & s ==>. t,S holds

s ==>. t,T

let s, t be Element of E ^omega ; :: thesis: ( S c= T & s ==>. t,S implies s ==>. t,T )

assume that

A1: S c= T and

A2: s ==>. t,S ; :: thesis: s ==>. t,T

consider v, w, s1, t1 being Element of E ^omega such that

A3: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w ) and

A4: s1 -->. t1,S by A2;

s1 -->. t1,T by A1, A4;

hence s ==>. t,T by A3; :: thesis: verum