theorem :: GLIBPRE1:114

for G being simple vertex-finite _Graph
for v being Vertex of G holds v .degree() < G .order()