let c be Cardinal; :: thesis: for G being simple c -regular _Graph holds c c= G .order()
let G be simple c -regular _Graph; :: thesis: c c= G .order()
set v = the Vertex of G;
card ( the Vertex of G .allNeighbors()) c= G .order() by CARD_1:11;
then the Vertex of G .degree() c= G .order() by GLIB_000:111;
hence c c= G .order() by Def4; :: thesis: verum