let G be _Graph; :: thesis: ( G is edgeless iff G is 0 -Dregular )
thus ( G is edgeless implies G is 0 -Dregular ) ; :: thesis: ( G is 0 -Dregular implies G is edgeless )
assume G is 0 -Dregular ; :: thesis: G is edgeless
then G is 2 * 0 -regular by Th46;
hence G is edgeless ; :: thesis: verum