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

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

A1: ==>.-relation ({} ((E ^omega),(E ^omega))) c= {} ((E ^omega),(E ^omega))

proof

{} ((E ^omega),(E ^omega)) = {}
by PARTIT_2:def 1;
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;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

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