let G be non-Dmulti _Graph; :: thesis: for E being RepDEdgeSelection of G holds E = the_Edges_of G

let E be RepDEdgeSelection of G; :: thesis: E = the_Edges_of G

for e being object st e in the_Edges_of G holds

e in E

hence E = the_Edges_of G by XBOOLE_0:def 10; :: thesis: verum

let E be RepDEdgeSelection of G; :: thesis: E = the_Edges_of G

for e being object st e in the_Edges_of G holds

e in E

proof

then
the_Edges_of G c= E
by TARSKI:def 3;
let e be object ; :: thesis: ( e in the_Edges_of G implies e in E )

set v = (the_Source_of G) . e;

set w = (the_Target_of G) . e;

assume e in the_Edges_of G ; :: thesis: e in E

then A1: e DJoins (the_Source_of G) . e,(the_Target_of G) . e,G by GLIB_000:def 14;

then consider e2 being object such that

A2: ( e2 DJoins (the_Source_of G) . e,(the_Target_of G) . e,G & e2 in E ) and

for e9 being object st e9 DJoins (the_Source_of G) . e,(the_Target_of G) . e,G & e9 in E holds

e9 = e2 by Def6;

thus e in E by A1, A2, GLIB_000:def 21; :: thesis: verum

end;set v = (the_Source_of G) . e;

set w = (the_Target_of G) . e;

assume e in the_Edges_of G ; :: thesis: e in E

then A1: e DJoins (the_Source_of G) . e,(the_Target_of G) . e,G by GLIB_000:def 14;

then consider e2 being object such that

A2: ( e2 DJoins (the_Source_of G) . e,(the_Target_of G) . e,G & e2 in E ) and

for e9 being object st e9 DJoins (the_Source_of G) . e,(the_Target_of G) . e,G & e9 in E holds

e9 = e2 by Def6;

thus e in E by A1, A2, GLIB_000:def 21; :: thesis: verum

hence E = the_Edges_of G by XBOOLE_0:def 10; :: thesis: verum