let G be _Graph; :: thesis: ( G is trivial & G is non-Dmulti implies G is finite )
assume A5: ( G is trivial & G is non-Dmulti ) ; :: thesis: G is finite
then card (the_Vertices_of G) = 1 by Def21;
then consider v being set such that
A6: the_Vertices_of G = {v} by CARD_2:60;

now

assume A7: not the_Edges_of G is finite ; :: thesis: contradiction
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));
A8: the_Edges_of G <> {} by A7;
( (the_Source_of G) . (choose (the_Edges_of G)) in the_Vertices_of G & (the_Target_of G) . (choose (the_Edges_of G)) in the_Vertices_of G ) by A7, FUNCT_2:7;
then ( (the_Source_of G) . (choose (the_Edges_of G)) = v & (the_Target_of G) . (choose (the_Edges_of G)) = v ) by A6, TARSKI:def 1;
then A9: choose (the_Edges_of G) DJoins v,v,G by A8, 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))} ) )

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 A8; :: thesis: verum

end;

assume A10: x in the_Edges_of G ; :: thesis: x in {(choose (the_Edges_of G))}
set v1 = (the_Source_of G) . x;
set v2 = (the_Target_of G) . x;
( (the_Source_of G) . x in the_Vertices_of G & (the_Target_of G) . x in the_Vertices_of G ) by A10, FUNCT_2:7;
then ( (the_Source_of G) . x = v & (the_Target_of G) . x = v ) by A6, TARSKI:def 1;
then x DJoins v,v,G by A10, Def16;
then x = choose (the_Edges_of G) by A5, A9, Def23;
hence x in {(choose (the_Edges_of G))} by TARSKI:def 1; :: thesis: verum

end;

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

end;

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