:: deftheorem Def7 defines regular GLIB_016:def 7 :
for G being locally-finite _Graph holds
( G is regular iff ex n being Nat st G is n -regular );