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

proof

let x be set ; :: 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 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, 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) by Def5;
[s1,t1] in id (E ^omega) by A6, Def4;
then s1 = t1 by RELAT_1:def 10;
hence x in id (E ^omega) by A4, A5, RELAT_1:def 10; :: thesis: verum

end;

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