let E be set ; 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; 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 ; ( S is Thue-system of E & s -->. t,S implies t -->. s,S )
assume
( S is Thue-system of E & s -->. t,S )
; 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
; verum