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;
then consider v being object such that
A9: the_Vertices_of G = {v} by CARD_2:42;

now :: thesis: the_Edges_of G is finite

set e1 = the Element of the_Edges_of G;
set v1 = (the_Source_of G) . the Element of the_Edges_of G;
set v2 = (the_Target_of G) . the Element of 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) . the Element of the_Edges_of G in the_Vertices_of G by A10, FUNCT_2:5;
then A12: (the_Target_of G) . the Element of the_Edges_of G = v by A9, TARSKI:def 1;
(the_Source_of G) . the Element of the_Edges_of G in the_Vertices_of G by A10, FUNCT_2:5;
then (the_Source_of G) . the Element of the_Edges_of G = v by A9, TARSKI:def 1;
then A13: the Element of the_Edges_of G DJoins v,v,G by A11, A12;

now :: thesis: for x being object holds
( ( x in { the Element of the_Edges_of G} implies x in the_Edges_of G ) & ( x in the_Edges_of G implies x in { the Element of the_Edges_of G} ) )

let x be object ; :: thesis: ( ( x in { the Element of the_Edges_of G} implies x in the_Edges_of G ) & ( x in the_Edges_of G implies x in { the Element of 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 { the Element of the_Edges_of G} )

assume x in { the Element of the_Edges_of G} ; :: thesis: x in the_Edges_of G
then x = the Element of 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 { the Element of 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;
then x = the Element of the_Edges_of G by A8, A13;
hence x in { the Element of the_Edges_of G} by TARSKI:def 1; :: thesis: verum

end;

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

end;

hence G is _finite by A9; :: thesis: verum