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))

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

(==>.-relation S) \/ (id (E ^omega)) c= ==>.-relation (S \/ (id (E ^omega)))
let x be object ; :: 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 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,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)) ;

A7: [s1,t1] in S \/ (id (E ^omega)) by A6;

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

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,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)) ;

A7: [s1,t1] in S \/ (id (E ^omega)) by A6;

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

end;

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

then
s1 -->. t1,S
;

then (v ^ s1) ^ w ==>. (v ^ t1) ^ w,S ;

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;then (v ^ s1) ^ w ==>. (v ^ t1) ^ w,S ;

then x in ==>.-relation S by A4, A5, Def6;

hence x in (==>.-relation S) \/ (id (E ^omega)) by XBOOLE_0:def 3; :: thesis: verum

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;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

proof

hence
==>.-relation (S \/ (id (E ^omega))) = (==>.-relation S) \/ (id (E ^omega))
by A1, XBOOLE_0:def 10; :: thesis: verum
let x be object ; :: 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)))

end;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;

end;

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;hence x in ==>.-relation (S \/ (id (E ^omega))) by A9; :: thesis: verum

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;x in ==>.-relation (id (E ^omega)) by A10, Th27;

hence x in ==>.-relation (S \/ (id (E ^omega))) by A11; :: thesis: verum