let G be _Graph; :: thesis: ( G is non-multi implies G is non-Dmulti )
assume A1: G is non-multi ; :: thesis: G is non-Dmulti
now :: thesis: for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds
e1 = e2
let e1, e2, v1, v2 be object ; :: thesis: ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G implies e1 = e2 )
assume ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ; :: thesis: e1 = e2
then ( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ;
hence e1 = e2 by A1; :: thesis: verum
end;
hence G is non-Dmulti ; :: thesis: verum