let G be _Graph; :: thesis: ( G is trivial & G is non-Dmulti implies G is finite )
assume that
A7: G is trivial and
A8: G is non-Dmulti ; :: thesis: G is finite
card (the_Vertices_of G) = 1 by A7, Def21;
then consider v being set such that
A9: the_Vertices_of G = {v} by CARD_2:42;

now

set e1 = choose (the_Edges_of G);
set v1 = (the_Source_of G) . (choose (the_Edges_of G));
set v2 = (the_Target_of G) . (choose (the_Edges_of G));
assume A10: not the_Edges_of G is finite ; :: thesis: contradiction
then A11: the_Edges_of G <> {} ;
(the_Target_of G) . (choose (the_Edges_of G)) in the_Vertices_of G by A10, FUNCT_2:5;
then A12: (the_Target_of G) . (choose (the_Edges_of G)) = v by A9, TARSKI:def 1;
(the_Source_of G) . (choose (the_Edges_of G)) in the_Vertices_of G by A10, FUNCT_2:5;
then (the_Source_of G) . (choose (the_Edges_of G)) = v by A9, TARSKI:def 1;
then A13: choose (the_Edges_of G) DJoins v,v,G by A11, A12, Def16;

now

let x be set ; :: thesis: ( ( x in {(choose (the_Edges_of G))} implies x in the_Edges_of G ) & ( x in the_Edges_of G implies x in {(choose (the_Edges_of G))} ) )
set v1 = (the_Source_of G) . x;
set v2 = (the_Target_of G) . x;

hereby :: thesis: ( x in the_Edges_of G implies x in {(choose (the_Edges_of G))} )

assume x in {(choose (the_Edges_of G))} ; :: thesis: x in the_Edges_of G
then x = choose (the_Edges_of G) by TARSKI:def 1;
hence x in the_Edges_of G by A11; :: thesis: verum

end;

assume A14: x in the_Edges_of G ; :: thesis: x in {(choose (the_Edges_of G))}
then (the_Target_of G) . x in the_Vertices_of G by FUNCT_2:5;
then A15: (the_Target_of G) . x = v by A9, TARSKI:def 1;
(the_Source_of G) . x in the_Vertices_of G by A14, FUNCT_2:5;
then (the_Source_of G) . x = v by A9, TARSKI:def 1;
then x DJoins v,v,G by A14, A15, Def16;
then x = choose (the_Edges_of G) by A8, A13, Def23;
hence x in {(choose (the_Edges_of G))} by TARSKI:def 1; :: thesis: verum

end;

hence contradiction by A10, TARSKI:1; :: thesis: verum

end;

hence G is finite by A9, Def19; :: thesis: verum