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

proof

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;

then the_Edges_of G c= E by TARSKI:def 3;
hence E = the_Edges_of G by XBOOLE_0:def 10; :: thesis: verum