let G be _Graph; :: thesis: ( G is _trivial & G is non-Dmulti & G is loopfull implies G is Cycle-like )
assume A1: ( G is _trivial & G is non-Dmulti & G is loopfull ) ; :: thesis: G is Cycle-like

now :: thesis: for v being Vertex of G holds v .degree() = 2

let v be Vertex of G; :: thesis: v .degree() = 2
A2: G .size() = 1

proof

consider e being object such that
A3: e Joins v,v,G by A1, GLIB_012:def 1;
A4: e in the_Edges_of G by A3, GLIB_000:def 13;
for e1, e2 being object st e1 in the_Edges_of G & e2 in the_Edges_of G holds
e1 = e2 by A1, ZFMISC_1:def 10;
then ex e9 being object st the_Edges_of G = {e9} by A4, ZFMISC_1:def 10, ZFMISC_1:131;
hence G .size() = 1 by CARD_1:30; :: thesis: verum

end;

thus v .degree() = 1 +` 1 by A1, A2, GLIB_000:149
.= 2 ; :: thesis: verum

end;

hence G is Cycle-like by A1, GLIB_016:def 4; :: thesis: verum