let G be _Graph; :: thesis: ( G is _trivial & G is 1 -edge implies G is 1 -Dregular )
assume A22: ( G is _trivial & G is 1 -edge ) ; :: thesis: G is 1 -Dregular
then G .order() = 1 by GLIB_000:26;
then consider v being Vertex of G such that
A23: the_Vertices_of G = {v} by GLIB_000:27;
G .size() = 1 by A22, GLIB_013:def 4;
then G .size() = card {{}} by CARD_1:30;
then consider e being object such that
A24: the_Edges_of G = {e} by CARD_1:29;
A25: ( v .edgesIn() c= {e} & v .edgesOut() c= {e} ) by A24;
e in the_Edges_of G by A24, TARSKI:def 1;
then A26: e Joins (the_Source_of G) . e,(the_Target_of G) . e,G by GLIB_000:def 13;
then ( (the_Source_of G) . e in {v} & (the_Target_of G) . e in {v} ) by A23, GLIB_000:13;
then ( (the_Source_of G) . e = v & (the_Target_of G) . e = v ) by TARSKI:def 1;
then ( e DJoins v,v,G & e is set ) by A26, GLIB_000:16, TARSKI:1;
then ( e in v .edgesIn() & e in v .edgesOut() ) by GLIB_000:57, GLIB_000:59;
then ( {e} c= v .edgesIn() & {e} c= v .edgesOut() ) by ZFMISC_1:31;
then ( {e} = v .edgesIn() & {e} = v .edgesOut() ) by A25, XBOOLE_0:def 10;
then A27: ( v .inDegree() = 1 & v .outDegree() = 1 ) by CARD_1:30;
let u be Vertex of G; :: according to GLIB_016:def 8 :: thesis: ( u .inDegree() = 1 & u .outDegree() = 1 )
u in {v} by A23;
hence ( u .inDegree() = 1 & u .outDegree() = 1 ) by A27, TARSKI:def 1; :: thesis: verum