theorem :: GLIB_016:25

for c being Cardinal
for G being simple b₁ -regular _Graph holds c c= G .order()