let G, e be set ; :: thesis: ( e in PairsOf G implies ex x, y being set st
( x <> y & x in union G & y in union G & e = {x,y} ) )
assume A1: e in PairsOf G ; :: thesis: ex x, y being set st
( x <> y & x in union G & y in union G & e = {x,y} )
then card e = 2 by Def1;
then consider x, y being object such that
A2: x <> y and
A3: e = {x,y} by CARD_2:60;
( x in e & y in e ) by A3, TARSKI:def 2;
then ( x in union G & y in union G ) by A1, TARSKI:def 4;
hence ex x, y being set st
( x <> y & x in union G & y in union G & e = {x,y} ) by A2, A3; :: thesis: verum