let E be RepDEdgeSelection of G; :: thesis: not E is empty
consider e0 being object such that
A3: e0 in the_Edges_of G by XBOOLE_0:def 1;
set v = (the_Source_of G) . e0;
set w = (the_Target_of G) . e0;
consider e being object such that
A4: ( e DJoins (the_Source_of G) . e0,(the_Target_of G) . e0,G & e in E ) and
for e9 being object st e9 DJoins (the_Source_of G) . e0,(the_Target_of G) . e0,G & e9 in E holds
e9 = e by A3, Def6, GLIB_000:def 14;
thus not E is empty by A4; :: thesis: verum