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

for s, t being Element of E ^omega st s ==>. t,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,S holds

s ==>* t,S

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

assume s ==>. t,S ; :: thesis: s ==>* t,S

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

then ==>.-relation S reduces s,t by REWRITE1:15;

hence s ==>* t,S ; :: thesis: verum

for s, t being Element of E ^omega st s ==>. t,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,S holds

s ==>* t,S

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

assume s ==>. t,S ; :: thesis: s ==>* t,S

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

then ==>.-relation S reduces s,t by REWRITE1:15;

hence s ==>* t,S ; :: thesis: verum