let G be _Graph; :: thesis:
assume that
A2: G is _trivial and
A3: G is loopless ; :: thesis:
card (the_Vertices_of G) = 1 by A2;
then consider v being object such that
A4: the_Vertices_of G = {v} by CARD_2:42;

suppose the_Edges_of G is empty ; :: thesis:

hence the_Edges_of G is finite ; :: thesis:

end;

suppose not the_Edges_of G is empty ; :: thesis:

then consider e being object such that
A5: e in the_Edges_of G by XBOOLE_0:def 1;
(the_Target_of G) . e in the_Vertices_of G by A5, FUNCT_2:5;
then A6: (the_Target_of G) . e = v by A4, TARSKI:def 1;
(the_Source_of G) . e in the_Vertices_of G by A5, FUNCT_2:5;
then (the_Source_of G) . e = v by A4, TARSKI:def 1;
hence the_Edges_of G is finite by A3, A5, A6; :: thesis:

end;

end;

end;

hence G is _finite by A4; :: thesis: