let G be non-Dmulti _Graph; :: thesis: G .size() c= (G .order()) *` (G .order())
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):] ) and
for e being object st e in dom f holds
f . e = [((the_Source_of G) . e),((the_Target_of G) . e)] by Th1;
G .size() c= card [:(the_Vertices_of G),(the_Vertices_of G):] by A1, CARD_1:10;
then G .size() c= card [:(G .order()),(card (the_Vertices_of G)):] by CARD_2:7;
hence G .size() c= (G .order()) *` (G .order()) by CARD_2:def 2; :: thesis: verum