consider G being finite trivial _Graph;
consider v being Vertex of G such that
A1: the_Vertices_of G = {v} by GLIB_000:25;

now

let W be Walk of G; :: thesis: ( W .length() > 3 implies not W is Cycle-like )
assume A2: ( W .length() > 3 & W is Cycle-like ) ; :: thesis: contradiction
2 * (W .length() ) > 2 * 3 by A2, XREAL_1:70;
then (2 * (W .length() )) + 1 > 6 + 1 by XREAL_1:10;
then A3: len W > 7 by GLIB_001:113;
reconsider j3 = (2 * 1) + 1 as odd Nat ;
reconsider j5 = (2 * 2) + 1 as odd Nat ;
A4: ( j3 <= len W & j5 <= len W ) by A3, XXREAL_0:2;
then ( W . j3 in W .vertices() & W . j5 in W .vertices() ) by GLIB_001:88;
then ( W . j3 = v & W . j5 = v ) by A1, TARSKI:def 1;
then not W is Path-like by A4, GLIB_001:def 28;
hence contradiction by A2; :: thesis: verum

end;

then for W being Walk of G st W .length() > 3 & W is Cycle-like holds
W is chordal ;
then G is chordal by Def11;
hence ex b₁ being _Graph st
( b₁ is trivial & b₁ is finite & b₁ is chordal ) ; :: thesis: verum