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 A1: ( S is Thue-system of E & s -->. t,S ) ; :: thesis: t -->. s,S
then A2: S = S ~ by RELAT_2:30;
[s,t] in S by A1, Def4;
then [t,s] in S by A2, RELAT_1:def 7;
hence t -->. s,S by Def4; :: thesis: verum