let G be _Graph; :: thesis: ( ex E being RepEdgeSelection of G st E = the_Edges_of G implies G is non-multi )
given E being RepEdgeSelection of G such that A1: E = the_Edges_of G ; :: thesis: G is non-multi

now :: thesis: for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2

let e1, e2, v1, v2 be object ; :: thesis: ( e1 Joins v1,v2,G & e2 Joins v1,v2,G implies e1 = e2 )
assume A2: ( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ; :: thesis: e1 = e2
then consider e3 being object such that
( e3 Joins v1,v2,G & e3 in E ) and
A3: for e being object st e Joins v1,v2,G & e in E holds
e = e3 by Def5;
( e1 in the_Edges_of G & e2 in the_Edges_of G & E = the_Edges_of G ) by A1, A2, GLIB_000:def 13;
then ( e1 = e3 & e2 = e3 ) by A2, A3;
hence e1 = e2 ; :: thesis: verum

end;

hence G is non-multi by GLIB_000:def 20; :: thesis: verum