let G be _Graph; :: thesis:
assume that
A7: G is _trivial and
A8: G is non-Dmulti ; :: thesis:
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:

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:
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:

let x be object ; :: thesis:
set v1 = (the_Source_of G) . x;
set v2 = (the_Target_of G) . x;

hereby :: thesis:

assume x in { the Element of the_Edges_of G} ; :: thesis:
then x = the Element of the_Edges_of G by TARSKI:def 1;
hence x in the_Edges_of G by A11; :: thesis:

end;

assume A14: x in the_Edges_of G ; :: thesis:
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:

end;

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

end;

hence G is _finite by A9; :: thesis: