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

now

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 set 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, Def20; :: thesis: verum

end;

end;

end;

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