let E be set ; :: thesis: for S being semi-Thue-system of E holds ==>.-relation (S \/ (id ())) = () \/ (id ())
let S be semi-Thue-system of E; :: thesis: ==>.-relation (S \/ (id ())) = () \/ (id ())
A1: ==>.-relation (S \/ (id ())) c= () \/ (id ())
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ==>.-relation (S \/ (id ())) or x in () \/ (id ()) )
assume A2: x in ==>.-relation (S \/ (id ())) ; :: thesis: x in () \/ (id ())
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 ()) 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 ()) ;
A7: [s1,t1] in S \/ (id ()) by A6;
per cases ( [s1,t1] in S or [s1,t1] in id () ) by ;
suppose [s1,t1] in S ; :: thesis: x in () \/ (id ())
then s1 -->. t1,S ;
then (v ^ s1) ^ w ==>. (v ^ t1) ^ w,S ;
then x in ==>.-relation S by A4, A5, Def6;
hence x in () \/ (id ()) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose [s1,t1] in id () ; :: thesis: x in () \/ (id ())
end;
end;
end;
(==>.-relation S) \/ (id ()) c= ==>.-relation (S \/ (id ()))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in () \/ (id ()) or x in ==>.-relation (S \/ (id ())) )
assume A8: x in () \/ (id ()) ; :: thesis: x in ==>.-relation (S \/ (id ()))
per cases ( x in ==>.-relation S or x in id () ) by ;
end;
end;
hence ==>.-relation (S \/ (id ())) = () \/ (id ()) by ; :: thesis: verum