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