:: deftheorem defines Dsimple GLIB_000:def 23 :
for G being _Graph holds
( G is Dsimple iff ( G is loopless & G is non-Dmulti ) );