let G be non-multi vertex-finite _Graph; :: thesis: G .size() <= (((G .order()) ^2) + (G .order())) / 2
set V1 = singletons (the_Vertices_of G);
set V2 = 2Set (the_Vertices_of G);
consider f being one-to-one Function such that
A1: ( dom f = the_Edges_of G & rng f c= (2Set (the_Vertices_of G)) \/ (singletons (the_Vertices_of G)) ) and
for e being object st e in dom f holds
f . e = {((the_Source_of G) . e),((the_Target_of G) . e)} by Th4;
reconsider n = (G .order()) - 1 as Nat by CHORD:1;
A2: card ((2Set (the_Vertices_of G)) \/ (singletons (the_Vertices_of G))) = (card (2Set (the_Vertices_of G))) +` (card (singletons (the_Vertices_of G))) by CARD_2:35, GLIBPRE0:18
.= (card (2Set (the_Vertices_of G))) +` (card (the_Vertices_of G)) by BSPACE:41
.= ((n + 1) choose 2) + (n + 1) by GLIBPRE0:20 ;
A3: ((n + 1) choose 2) + (n + 1) = ((n * (n + 1)) / 2) + ((2 * (n + 1)) / 2) by NUMPOLY1:72
.= (((G .order()) * (G .order())) + (G .order())) / 2
.= (((G .order()) ^2) + (G .order())) / 2 by SQUARE_1:def 1 ;
card (rng f) c= ((n + 1) choose 2) + (n + 1) by A1, A2, CARD_1:11;
then Segm (G .size()) c= Segm (((n + 1) choose 2) + (n + 1)) by A1, CARD_1:70;
hence G .size() <= (((G .order()) ^2) + (G .order())) / 2 by A3, NAT_1:39; :: thesis: verum