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 :: thesis: for x being object holds
( ( x in ==>.-relation S implies x in (==>.-relation S) ~ ) & ( x in (==>.-relation S) ~ implies x in ==>.-relation S ) )

let x be object ; :: 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 object such that
A3: ( a in E ^omega & b in E ^omega ) and
A4: 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, A4, Def6;
then b ==>. a,S by A1, Th17;
then [b,a] in ==>.-relation S by Def6;
hence x in (==>.-relation S) ~ by A4, RELAT_1:def 7; :: thesis: verum

end;

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

proof

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

end;

end;

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