let E be RepEdgeSelection of G; :: thesis: E is empty
the_Edges_of G = {} ;
hence E is empty by XBOOLE_1:3; :: thesis: verum