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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ==>.-relation ({} ((E ^omega),(E ^omega))) or x in {} ((E ^omega),(E ^omega)) )
assume A2: x in ==>.-relation ({} ((E ^omega),(E ^omega))) ; :: thesis: x in {} ((E ^omega),(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, {} ((E ^omega),(E ^omega)) by A2, A4, Def6;
hence x in {} ((E ^omega),(E ^omega)) by Th20; :: thesis: verum

end;

{} ((E ^omega),(E ^omega)) = {} by PARTIT_2:def 1;
then {} ((E ^omega),(E ^omega)) c= ==>.-relation ({} ((E ^omega),(E ^omega))) ;
hence ==>.-relation ({} ((E ^omega),(E ^omega))) = {} ((E ^omega),(E ^omega)) by A1, XBOOLE_0:def 10; :: thesis: verum