theorem :: GLIB_009:70

for G being _Graph holds
( G is non-multi iff EdgeAdjEqRel G = id (the_Edges_of G) )