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

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
A4: e in the_Edges_of G by XBOOLE_0:def 1;
( (the_Source_of G) . e in the_Vertices_of G & (the_Target_of G) . e in the_Vertices_of G ) by A4, FUNCT_2:7;
then ( (the_Source_of G) . e = v & (the_Target_of G) . e = v ) by A3, TARSKI:def 1;
hence the_Edges_of G is finite by A2, A4, Def20; :: thesis: verum

end;

end;

end;

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