let E be set ; :: thesis: for S being semi-Thue-system of E
for s, t being Element of E ^omega st S is Thue-system of E & s ==>. t,S holds
t ==>. s,S
let S be semi-Thue-system of E; :: thesis: for s, t being Element of E ^omega st S is Thue-system of E & s ==>. t,S holds
t ==>. s,S
let s, t be Element of E ^omega ; :: thesis: ( S is Thue-system of E & s ==>. t,S implies t ==>. s,S )
assume that
A1: S is Thue-system of E and
A2: s ==>. t,S ; :: thesis: t ==>. s,S
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, Def5;
t1 -->. s1,S by A1, A4, Th16;
hence t ==>. s,S by A3, Def5; :: thesis: verum