theorem :: GLIB_013:11

for G being non-multi vertex-finite _Graph holds G .size() <= (((G .order()) ^2) + (G .order())) / 2