let G be _Graph; :: thesis: ( G is edgeless iff G is 0 -regular )
thus ( G is edgeless implies G is 0 -regular ) ; :: thesis: ( G is 0 -regular implies G is edgeless )
assume A1: G is 0 -regular ; :: thesis: G is edgeless
assume not G is edgeless ; :: thesis: contradiction
then consider e being object such that
A2: e in the_Edges_of G by XBOOLE_0:def 1;
A3: e Joins (the_Source_of G) . e,(the_Target_of G) . e,G by A2, GLIB_000:def 13;
then reconsider v = (the_Source_of G) . e as Vertex of G by GLIB_000:13;
v .degree() <> 0 by A3, GLIB_000:143, GLIB_000:157;
hence contradiction by A1; :: thesis: verum