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

let S be semi-Thue-system of E; :: thesis: ( S is Thue-system of E implies ==>.-relation S = () ~ )
assume A1: S is Thue-system of E ; :: thesis:
now :: thesis: for x being object holds
( ( x in ==>.-relation S implies x in () ~ ) & ( x in () ~ implies x in ==>.-relation S ) )
let x be object ; :: thesis: ( ( x in ==>.-relation S implies x in () ~ ) & ( x in () ~ implies x in ==>.-relation S ) )
thus ( x in ==>.-relation S implies x in () ~ ) :: thesis: ( x in () ~ implies x in ==>.-relation S )
proof
assume A2: x in ==>.-relation S ; :: thesis: x in () ~
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 ;
then [b,a] in ==>.-relation S by Def6;
hence x in () ~ by ; :: thesis: verum
end;
thus ( x in () ~ implies x in ==>.-relation S ) :: thesis: verum
proof
assume A5: x in () ~ ; :: thesis:
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 ;
then b ==>. a,S by Def6;
then a ==>. b,S by ;
hence x in ==>.-relation S by ; :: thesis: verum
end;
end;
hence ==>.-relation S = () ~ by TARSKI:2; :: thesis: verum