theorem :: GLIBPRE1:113

for G being Dsimple vertex-finite _Graph
for v being Vertex of G holds
( v .inDegree() < G .order() & v .outDegree() < G .order() )