let c be Cardinal; :: thesis: for G being Dsimple c -Dregular _Graph holds c c= G .order()
let G be Dsimple c -Dregular _Graph; :: thesis: c c= G .order()
set v = the Vertex of G;
card ( the Vertex of G .inNeighbors()) c= G .order() by CARD_1:11;
then the Vertex of G .inDegree() c= G .order() by GLIB_000:109;
hence c c= G .order() by Def8; :: thesis: verum