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

let e1, e2, v1, v2 be set ; :: 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 ) by Lm2;
hence e1 = e2 by A1, Def22; :: thesis: verum

end;

hence G is non-Dmulti by Def23; :: thesis: verum