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

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