let G be _Graph; :: thesis: ( G is vertex-finite & G is non-Dmulti implies G is edge-finite )
assume A1: ( G is vertex-finite & G is non-Dmulti ) ; :: thesis: G is edge-finite
then A2: G .size() c= (G .order()) *` (G .order()) by Th2;
reconsider X = G .order() as finite set by A1;
(G .order()) *` (G .order()) = card [:(G .order()),(G .order()):] by CARD_2:def 2
.= (card X) * (card X) by CARD_2:46 ;
hence G is edge-finite by A2; :: thesis: verum