let E be set ; :: thesis: for S being semi-Thue-system of E holds ==>.-relation (S \/ (id (E ^omega ))) = (==>.-relation S) \/ (id (E ^omega ))
let S be semi-Thue-system of E; :: thesis: ==>.-relation (S \/ (id (E ^omega ))) = (==>.-relation S) \/ (id (E ^omega ))
A1: ==>.-relation (S \/ (id (E ^omega ))) c= (==>.-relation S) \/ (id (E ^omega ))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ==>.-relation (S \/ (id (E ^omega ))) or x in (==>.-relation S) \/ (id (E ^omega )) )
assume A2: x in ==>.-relation (S \/ (id (E ^omega ))) ; :: thesis: x in (==>.-relation S) \/ (id (E ^omega ))
then consider a, b being set such that
A3: ( a in E ^omega & b in E ^omega & x = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of E ^omega by A3;
a ==>. b,S \/ (id (E ^omega )) by A2, A3, Def6;
then consider v, w, s1, t1 being Element of E ^omega such that
A4: ( a = (v ^ s1) ^ w & b = (v ^ t1) ^ w & s1 -->. t1,S \/ (id (E ^omega )) ) by Def5;
A5: [s1,t1] in S \/ (id (E ^omega )) by A4, Def4;

per cases ( [s1,t1] in S or [s1,t1] in id (E ^omega ) ) by A5, XBOOLE_0:def 3;

suppose [s1,t1] in S ; :: thesis: x in (==>.-relation S) \/ (id (E ^omega ))

then s1 -->. t1,S by Def4;
then (v ^ s1) ^ w ==>. (v ^ t1) ^ w,S by Th15;
then x in ==>.-relation S by A3, A4, Def6;
hence x in (==>.-relation S) \/ (id (E ^omega )) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose [s1,t1] in id (E ^omega ) ; :: thesis: x in (==>.-relation S) \/ (id (E ^omega ))

then s1 = t1 by RELAT_1:def 10;
then x in id (E ^omega ) by A3, A4, RELAT_1:def 10;
hence x in (==>.-relation S) \/ (id (E ^omega )) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

(==>.-relation S) \/ (id (E ^omega )) c= ==>.-relation (S \/ (id (E ^omega )))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (==>.-relation S) \/ (id (E ^omega )) or x in ==>.-relation (S \/ (id (E ^omega ))) )
assume A6: x in (==>.-relation S) \/ (id (E ^omega )) ; :: thesis: x in ==>.-relation (S \/ (id (E ^omega )))

per cases ( x in ==>.-relation S or x in id (E ^omega ) ) by A6, XBOOLE_0:def 3;

suppose A7: x in ==>.-relation S ; :: thesis: x in ==>.-relation (S \/ (id (E ^omega )))

==>.-relation S c= ==>.-relation (S \/ (id (E ^omega ))) by Th26, XBOOLE_1:7;
hence x in ==>.-relation (S \/ (id (E ^omega ))) by A7; :: thesis: verum

end;

suppose x in id (E ^omega ) ; :: thesis: x in ==>.-relation (S \/ (id (E ^omega )))

then A8: x in ==>.-relation (id (E ^omega )) by Th27;
==>.-relation (id (E ^omega )) c= ==>.-relation (S \/ (id (E ^omega ))) by Th26, XBOOLE_1:7;
hence x in ==>.-relation (S \/ (id (E ^omega ))) by A8; :: thesis: verum

end;

end;

end;

hence ==>.-relation (S \/ (id (E ^omega ))) = (==>.-relation S) \/ (id (E ^omega )) by A1, XBOOLE_0:def 10; :: thesis: verum