:: deftheorem defines Dsimple GLIB_014:def 7 :
for S being Graph-membered set holds
( S is Dsimple iff for G being _Graph st G in S holds
G is Dsimple );