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