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 A: e in PairsOf G ; :: thesis: ex x, y being set st
( x <> y & x in union G & y in union G & e = {x,y} )
card e = 2 by A, LEdges;
then consider x, y being set such that
D: x <> y and
E: e = {x,y} by CARD_2:60;
( x in e & y in e ) by E, TARSKI:def 2;
then ( x in union G & y in union G ) by A, TARSKI:def 4;
hence ex x, y being set st
( x <> y & x in union G & y in union G & e = {x,y} ) by D, E; :: thesis: verum