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

let S be semi-Thue-system of E; :: thesis: ==>.-relation (==>.-relation S) = ==>.-relation S

A1: ==>.-relation (==>.-relation S) c= ==>.-relation S

hence ==>.-relation (==>.-relation S) = ==>.-relation S by A1, XBOOLE_0:def 10; :: thesis: verum

let S be semi-Thue-system of E; :: thesis: ==>.-relation (==>.-relation S) = ==>.-relation S

A1: ==>.-relation (==>.-relation S) c= ==>.-relation S

proof

==>.-relation S c= ==>.-relation (==>.-relation S)
by Th22;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ==>.-relation (==>.-relation S) or x in ==>.-relation S )

assume A2: x in ==>.-relation (==>.-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, ==>.-relation S by A2, A4, Def6;

then a ==>. b,S by Th30;

hence x in ==>.-relation S by A4, Def6; :: thesis: verum

end;assume A2: x in ==>.-relation (==>.-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, ==>.-relation S by A2, A4, Def6;

then a ==>. b,S by Th30;

hence x in ==>.-relation S by A4, Def6; :: thesis: verum

hence ==>.-relation (==>.-relation S) = ==>.-relation S by A1, XBOOLE_0:def 10; :: thesis: verum