let G be _Graph; ( ex E being RepDEdgeSelection of G st E = the_Edges_of G implies G is non-Dmulti )
given E being RepDEdgeSelection of G such that A1:
E = the_Edges_of G
; G is non-Dmulti
now for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds
e1 = e2let e1,
e2,
v1,
v2 be
object ;
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G implies e1 = e2 )assume A2:
(
e1 DJoins v1,
v2,
G &
e2 DJoins v1,
v2,
G )
;
e1 = e2then consider e3 being
object such that
(
e3 DJoins v1,
v2,
G &
e3 in E )
and A3:
for
e being
object st
e DJoins v1,
v2,
G &
e in E holds
e = e3
by Def6;
(
e1 = e3 &
e2 = e3 )
by A1, A2, A3, GLIB_000:def 14;
hence
e1 = e2
;
verum end;
hence
G is non-Dmulti
by GLIB_000:def 21; verum