let G be _Graph; :: thesis: ( G is _trivial & G is Cycle-like implies ( G is non-multi & G is loopfull ) )
assume A6: ( G is _trivial & G is Cycle-like ) ; :: thesis: ( G is non-multi & G is loopfull )
then 1 = G .order() by GLIB_000:26
.= G .size() by A6, Th40 ;
then consider e being object such that
A7: the_Edges_of G = {e} by CARD_2:42;

now :: thesis: for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2

let e1, e2, v1, v2 be object ; :: thesis: ( e1 Joins v1,v2,G & e2 Joins v1,v2,G implies e1 = e2 )
assume ( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ; :: thesis: e1 = e2
then ( e1 in the_Edges_of G & e2 in the_Edges_of G ) by GLIB_000:def 13;
hence e1 = e2 by A7, ZFMISC_1:def 10; :: thesis: verum

end;

hence G is non-multi by GLIB_000:def 20; :: thesis: G is loopfull

now :: thesis: for v being Vertex of G ex e being object st e Joins v,v,G

let v be Vertex of G; :: thesis: ex e being object st e Joins v,v,G
take e = e; :: thesis: e Joins v,v,G
set u = (the_Source_of G) . e;
set w = (the_Target_of G) . e;
e in the_Edges_of G by A7, TARSKI:def 1;
then A8: e Joins (the_Source_of G) . e,(the_Target_of G) . e,G by GLIB_000:def 13;
then reconsider u = (the_Source_of G) . e, w = (the_Target_of G) . e as Vertex of G by GLIB_000:13;
( v = u & v = w ) by A6, ZFMISC_1:def 10;
hence e Joins v,v,G by A8; :: thesis: verum

end;

hence G is loopfull by GLIB_012:def 1; :: thesis: verum