let G be non-Dmulti vertex-finite _Graph; :: thesis: G .size() <= (G .order()) ^2
(G .order()) *` (G .order()) = card [:(G .order()),(G .order()):] by CARD_2:def 2
.= (card (G .order())) * (G .order()) by CARD_2:46
.= Segm ((G .order()) * (G .order())) ;
then Segm (G .size()) c= Segm ((G .order()) * (G .order())) by Th2;
then G .size() <= (G .order()) * (G .order()) by NAT_1:39;
hence G .size() <= (G .order()) ^2 by SQUARE_1:def 1; :: thesis: verum