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

proof

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;

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