theorem :: GLIB_013:10

for G being Dsimple vertex-finite _Graph holds G .size() <= ((G .order()) ^2) - (G .order())