let G be simple vertex-finite _Graph; :: thesis: G .size() <= (((G .order()) ^2) - (G .order())) / 2
consider f being one-to-one Function such that
A1: ( dom f = the_Edges_of G & rng f c= 2Set (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 Th5;
reconsider n = (G .order()) - 1 as Nat by CHORD:1;
A2: card (2Set (the_Vertices_of G)) = (card (the_Vertices_of G)) choose 2 by GLIBPRE0:20
.= (n * (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= card (2Set (the_Vertices_of G)) by A1, CARD_1:11;
then Segm (G .size()) c= Segm (card (2Set (the_Vertices_of G))) by A1, CARD_1:70;
hence G .size() <= (((G .order()) ^2) - (G .order())) / 2 by A2, NAT_1:39; :: thesis: verum