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 ==>.-relation (==>.-relation S) reduces s,t by Def7;
then ==>.-relation S reduces s,t by Th31;
hence s ==>* t,S by Def7; :: thesis: verum