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

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

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

assume A1: x in S ; :: thesis: x in ==>.-relation S

then consider a, b being object such that

A2: ( a in E ^omega & b in E ^omega ) and

A3: x = [a,b] by ZFMISC_1:def 2;

reconsider a = a, b = b as Element of E ^omega by A2;

a -->. b,S by A1, A3;

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

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

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

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

assume A1: x in S ; :: thesis: x in ==>.-relation S

then consider a, b being object such that

A2: ( a in E ^omega & b in E ^omega ) and

A3: x = [a,b] by ZFMISC_1:def 2;

reconsider a = a, b = b as Element of E ^omega by A2;

a -->. b,S by A1, A3;

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

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