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