let G be _Graph; :: thesis: ( G is _trivial & G is loopless implies G is _finite )
assume that
A2: G is _trivial and
A3: G is loopless ; :: thesis: G is _finite
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;

now :: thesis: the_Edges_of G is finite

per cases ( the_Edges_of G is empty or not the_Edges_of G is empty ) ;

suppose the_Edges_of G is empty ; :: thesis: the_Edges_of G is finite

hence the_Edges_of G is finite ; :: thesis: verum

end;

suppose not the_Edges_of G is empty ; :: thesis: the_Edges_of G is finite

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

end;

end;

end;

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