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

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