let G be _Graph; :: thesis: ( G is c -Dregular implies not G is edgeless )
assume A1: G is c -Dregular ; :: thesis: not G is edgeless
set v = the Vertex of G;
the Vertex of G .inDegree() = c by A1;
hence not G is edgeless ; :: thesis: verum