let G be _Graph; ( 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
; G is non-multi
now for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2let e1,
e2,
v1,
v2 be
object ;
( 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 )
;
e1 = e2then 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
;
verum end;
hence
G is non-multi
by GLIB_000:def 20; verum