let E be set ; :: thesis: ==>.-relation ({} (E ^omega ),(E ^omega )) = {} (E ^omega ),(E ^omega )
{} (E ^omega ),(E ^omega ) = {} by OPOSET_1:def 1;
then A1: {} (E ^omega ),(E ^omega ) c= ==>.-relation ({} (E ^omega ),(E ^omega )) by XBOOLE_1:2;
==>.-relation ({} (E ^omega ),(E ^omega )) c= {} (E ^omega ),(E ^omega )

proof

let x be set ; :: 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 set such that
A3: ( a in E ^omega & b in E ^omega & 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, A3, Def6;
hence x in {} (E ^omega ),(E ^omega ) by Th20; :: thesis: verum

end;

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