let G be _Graph; :: thesis: ( not G is _trivial & G is Cycle-like implies G is loopless )
assume A9: ( not G is _trivial & G is Cycle-like ) ; :: thesis: G is loopless
then consider C being Walk of G such that
A10: C is Cycle-like by GLIB_002:def 2;
assume not G is loopless ; :: thesis: contradiction
then consider v, e being object such that
A11: e Joins v,v,G by GLIB_000:18;
e in the_Edges_of G by A11, GLIB_000:def 13;
then e in C .edges() by A9, A10, Th39;
then consider n being odd Element of NAT such that
A12: ( n < len C & C . (n + 1) = e ) by GLIB_001:100;
C . (n + 1) Joins C . n,C . (n + 2),G by A12, GLIB_001:def 3;
then A13: ( C . n = v & C . (n + 2) = v ) by A11, A12, GLIB_000:15;
A14: n + 0 < n + 2 by XREAL_1:8;
n + 2 <= len C by A12, CHORD:4;
then ( n = 1 & n + 2 = len C ) by A10, A13, A14, GLIB_001:def 28;
then 2 + 1 = (2 * (C .length())) + 1 by GLIB_001:112;
then 1 = card (C .edges()) by A10, Th4
.= G .size() by A9, A10, Th39
.= G .order() by A9, Th40 ;
hence contradiction by A9, GLIB_000:26; :: thesis: verum