let E be set ; :: thesis: for S being semi-Thue-system of E st S is Thue-system of E holds
==>.-relation S = (==>.-relation S) ~
let S be semi-Thue-system of E; :: thesis: ( S is Thue-system of E implies ==>.-relation S = (==>.-relation S) ~ )
assume A1: S is Thue-system of E ; :: thesis: ==>.-relation S = (==>.-relation S) ~

now

let x be set ; :: thesis: ( ( x in ==>.-relation S implies x in (==>.-relation S) ~ ) & ( x in (==>.-relation S) ~ implies x in ==>.-relation S ) )
thus ( x in ==>.-relation S implies x in (==>.-relation S) ~ ) :: thesis: ( x in (==>.-relation S) ~ implies x in ==>.-relation S )

proof

assume A2: x in ==>.-relation S ; :: thesis: x in (==>.-relation S) ~
then consider a, b being set such that
A3: ( a in E ^omega & b in E ^omega & x = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of E ^omega by A3;
a ==>. b,S by A2, A3, Def6;
then b ==>. a,S by A1, Th17;
then [b,a] in ==>.-relation S by Def6;
hence x in (==>.-relation S) ~ by A3, RELAT_1:def 7; :: thesis: verum

end;

thus ( x in (==>.-relation S) ~ implies x in ==>.-relation S ) :: thesis: verum

proof

assume A4: x in (==>.-relation S) ~ ; :: thesis: x in ==>.-relation S
then consider a, b being set such that
A5: ( a in E ^omega & b in E ^omega & x = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of E ^omega by A5;
[b,a] in ==>.-relation S by A4, A5, RELAT_1:def 7;
then b ==>. a,S by Def6;
then a ==>. b,S by A1, Th17;
hence x in ==>.-relation S by A5, Def6; :: thesis: verum

end;

end;

hence ==>.-relation S = (==>.-relation S) ~ by TARSKI:2; :: thesis: verum