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

for s, t being Element of E ^omega st s ==>. t, ==>.-relation S holds

s ==>. t,S

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

s ==>. t,S

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

assume s ==>. t, ==>.-relation S ; :: thesis: s ==>. t,S

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

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

A2: s1 -->. t1, ==>.-relation S ;

[s1,t1] in ==>.-relation S by A2;

then s1 ==>. t1,S by Def6;

hence s ==>. t,S by A1, Th13; :: thesis: verum

for s, t being Element of E ^omega st s ==>. t, ==>.-relation S holds

s ==>. t,S

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

s ==>. t,S

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

assume s ==>. t, ==>.-relation S ; :: thesis: s ==>. t,S

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

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

A2: s1 -->. t1, ==>.-relation S ;

[s1,t1] in ==>.-relation S by A2;

then s1 ==>. t1,S by Def6;

hence s ==>. t,S by A1, Th13; :: thesis: verum