let E be set ; :: thesis: ==>.-relation (id (E ^omega)) = id (E ^omega)

A1: ==>.-relation (id (E ^omega)) c= id (E ^omega)

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

A1: ==>.-relation (id (E ^omega)) c= id (E ^omega)

proof

id (E ^omega) c= ==>.-relation (id (E ^omega))
by Th22;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ==>.-relation (id (E ^omega)) or x in id (E ^omega) )

assume A2: x in ==>.-relation (id (E ^omega)) ; :: thesis: x in 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, 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, id (E ^omega) ;

[s1,t1] in id (E ^omega) by A6;

then s1 = t1 by RELAT_1:def 10;

hence x in id (E ^omega) by A4, A5, RELAT_1:def 10; :: thesis: verum

end;assume A2: x in ==>.-relation (id (E ^omega)) ; :: thesis: x in 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, 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, id (E ^omega) ;

[s1,t1] in id (E ^omega) by A6;

then s1 = t1 by RELAT_1:def 10;

hence x in id (E ^omega) by A4, A5, RELAT_1:def 10; :: thesis: verum

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