theorem :: GLIB_009:71

for G being _Graph holds
( G is non-Dmulti iff DEdgeAdjEqRel G = id (the_Edges_of G) )