let G be _Graph; :: thesis: ( G is non-Dmulti iff DEdgeAdjEqRel G = id (the_Edges_of G) )

hereby :: thesis: ( DEdgeAdjEqRel G = id (the_Edges_of G) implies G is non-Dmulti )

assume A1: G is non-Dmulti ; :: thesis: DEdgeAdjEqRel G = id (the_Edges_of G)

now :: thesis: for e1, e2 being object holds
( ( [e1,e2] in DEdgeAdjEqRel G implies [e1,e2] in id (the_Edges_of G) ) & ( [e1,e2] in id (the_Edges_of G) implies [e1,e2] in DEdgeAdjEqRel G ) )

let e1, e2 be object ; :: thesis: ( ( [e1,e2] in DEdgeAdjEqRel G implies [e1,e2] in id (the_Edges_of G) ) & ( [e1,e2] in id (the_Edges_of G) implies [e1,e2] in DEdgeAdjEqRel G ) )

hereby :: thesis: ( [e1,e2] in id (the_Edges_of G) implies [e1,e2] in DEdgeAdjEqRel G )

assume [e1,e2] in DEdgeAdjEqRel G ; :: thesis: [e1,e2] in id (the_Edges_of G)
then consider v1, v2 being object such that
A2: ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) by Def4;
A3: e1 = e2 by A1, A2, GLIB_000:def 21;
( e1 in the_Edges_of G & e2 in the_Edges_of G ) by A2, GLIB_000:def 14;
hence [e1,e2] in id (the_Edges_of G) by A3, RELAT_1:def 10; :: thesis: verum

end;

assume [e1,e2] in id (the_Edges_of G) ; :: thesis: [e1,e2] in DEdgeAdjEqRel G
then A4: ( e1 in the_Edges_of G & e1 = e2 ) by RELAT_1:def 10;

now :: thesis: ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G )

reconsider v1 = (the_Source_of G) . e1, v2 = (the_Target_of G) . e1 as object ;
take v1 = v1; :: thesis: ex v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G )
take v2 = v2; :: thesis: ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G )
thus ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) by A4, GLIB_000:def 14; :: thesis: verum

end;

hence [e1,e2] in DEdgeAdjEqRel G by Def4; :: thesis: verum

end;

hence DEdgeAdjEqRel G = id (the_Edges_of G) by RELAT_1:def 2; :: thesis: verum

end;

assume A5: DEdgeAdjEqRel G = id (the_Edges_of G) ; :: 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,e2] in DEdgeAdjEqRel G by Def4;
hence e1 = e2 by A5, RELAT_1:def 10; :: thesis: verum

end;

hence G is non-Dmulti by GLIB_000:def 21; :: thesis: verum