let C be Component of G; :: thesis: C is c -Dregular
let w be Vertex of C; :: according to GLIB_016:def 8 :: thesis: ( w .inDegree() = c & w .outDegree() = c )
the_Vertices_of C c= the_Vertices_of G ;
then reconsider v = w as Vertex of G by TARSKI:def 3;
thus w .inDegree() = v .inDegree() by GLIBPRE0:44
.= c by Def8 ; :: thesis: w .outDegree() = c
thus w .outDegree() = v .outDegree() by GLIBPRE0:44
.= c by Def8 ; :: thesis: verum