:: deftheorem Def6 defines regular GLIB_016:def 6 :
for G being _Graph holds
( G is regular iff ex c being Cardinal st G is c -regular );