let E be RepEdgeSelection of G; :: thesis: not E is empty
consider e0 being object such that
A1: 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;
e0 Joins (the_Source_of G) . e0,(the_Target_of G) . e0,G by A1, GLIB_000:def 13;
then consider e being object such that
A2: ( e Joins (the_Source_of G) . e0,(the_Target_of G) . e0,G & e in E ) and
for e9 being object st e9 Joins (the_Source_of G) . e0,(the_Target_of G) . e0,G & e9 in E holds
e9 = e by Def5;
thus not E is empty by A2; :: thesis: verum