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 ( S is Thue-system of E & s -->. t,S ) ; :: thesis: t -->. s,S

then ( S = S ~ & [s,t] in S ) by RELAT_2:13;

then [t,s] in S by RELAT_1:def 7;

hence t -->. s,S ; :: thesis: verum

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 ( S is Thue-system of E & s -->. t,S ) ; :: thesis: t -->. s,S

then ( S = S ~ & [s,t] in S ) by RELAT_2:13;

then [t,s] in S by RELAT_1:def 7;

hence t -->. s,S ; :: thesis: verum