theorem Th47: :: GLIB_016:47

for G being _Graph holds
( G is edgeless iff G is 0 -Dregular )