:: deftheorem Def20 defines non-multi GLIB_000:def 20 :
for G being _Graph holds
( G is non-multi iff for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2 );