consider c being Cardinal such that
A1: G is c -Dregular by Def9;
thus for b₁ being Vertex of G holds not b₁ is endvertex by A1; :: thesis: verum