let G be Dsimple vertex-finite _Graph; :: thesis: G .size() <= ((G .order()) ^2) - (G .order())
set P = [:(the_Vertices_of G),(the_Vertices_of G):];
set I = id (the_Vertices_of G);
consider f being one-to-one Function such that
A1: ( dom f = the_Edges_of G & rng f c= [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (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 Th3;
A2: (G .order()) - 1 is Nat by CHORD:1;
((G .order()) ^2) - (G .order()) = ((G .order()) * (G .order())) - (G .order()) by SQUARE_1:def 1
.= (G .order()) * ((G .order()) - 1) ;
then A3: ((G .order()) ^2) - (G .order()) is Nat by A2;
card ([:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G))) = (card [:(the_Vertices_of G),(the_Vertices_of G):]) - (card (id (the_Vertices_of G))) by CARD_2:44
.= ((G .order()) * (card (the_Vertices_of G))) - (card (id (the_Vertices_of G))) by CARD_2:46
.= ((G .order()) ^2) - (card (id (the_Vertices_of G))) by SQUARE_1:def 1
.= ((G .order()) ^2) - (card (dom (id (the_Vertices_of G)))) by CARD_1:62
.= ((G .order()) ^2) - (G .order()) ;
then Segm (G .size()) c= Segm (((G .order()) ^2) - (G .order())) by A1, CARD_1:10;
hence G .size() <= ((G .order()) ^2) - (G .order()) by A3, NAT_1:39; :: thesis: verum