let G be _Graph; :: thesis: ( G is _trivial & G is non-Dmulti implies G is non-multi )
assume A1: ( G is _trivial & G is non-Dmulti ) ; :: thesis: G is non-multi
then consider v being Vertex of G such that
A2: the_Vertices_of G = {v} by Th22;
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 ; :: thesis: ( 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 ) ; :: thesis: e1 = e2
then ( v1 in the_Vertices_of G & v2 in the_Vertices_of G ) by FUNCT_2:5;
then ( v1 = v & v2 = v ) by A2, TARSKI:def 1;
then ( e1 DJoins v,v,G & e2 DJoins v,v,G ) by A3;
hence e1 = e2 by A1; :: thesis: verum

end;

hence G is non-multi ; :: thesis: verum