let G be _Graph; ( G is _trivial & G is non-Dmulti implies G is non-multi )
assume A1:
( G is _trivial & G is non-Dmulti )
; G is non-multi
then consider v being Vertex of G such that
A2:
the_Vertices_of G = {v}
by GLIB_000:22;
for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2
proof
let e1,
e2,
v1,
v2 be
object ;
( e1 Joins v1,v2,G & e2 Joins v1,v2,G implies e1 = e2 )
assume A3:
(
e1 Joins v1,
v2,
G &
e2 Joins v1,
v2,
G )
;
e1 = e2
then
(
v1 in the_Vertices_of G &
v2 in the_Vertices_of G )
by GLIB_000:13;
then
(
v1 = v &
v2 = v )
by A2, TARSKI:def 1;
then
(
e1 DJoins v,
v,
G &
e2 DJoins v,
v,
G )
by A3, GLIB_000:16;
hence
e1 = e2
by A1, GLIB_000:def 21;
verum
end;
hence
G is non-multi
by GLIB_000:def 20; verum