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 ) and
A4: 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, A4, Def6;
then consider v, w, s1, t1 being Element of E ^omega such that
A5: ( a = (v ^ s1) ^ w & b = (v ^ t1) ^ w ) and
A6: s1 -->. t1,S \/ (id (E ^omega)) by Def5;
A7: [s1,t1] in S \/ (id (E ^omega)) by A6, Def4;

per cases ( [s1,t1] in S or [s1,t1] in id (E ^omega) ) by A7, 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 A4, A5, 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 A4, A5, 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 A8: 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 A8, XBOOLE_0:def 3;

suppose A9: 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 A9; :: thesis: verum

end;

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

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

end;

end;

end;

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