:: deftheorem Def9 defines Dregular GLIB_016:def 9 :
for G being _Graph holds
( G is Dregular iff ex c being Cardinal st G is c -Dregular );