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

reconsider j5 = (2 * 2) + 1 as odd Nat ;
reconsider j3 = (2 * 1) + 1 as odd Nat ;
let W be Walk of G; :: thesis: ( W .length() > 3 implies not W is Cycle-like )
assume that
A2: W .length() > 3 and
A3: 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 A4: len W > 7 by GLIB_001:113;
then j3 <= len W by XXREAL_0:2;
then W . j3 in W .vertices() by GLIB_001:88;
then A5: W . j3 = v by A1, TARSKI:def 1;
A6: j5 <= len W by A4, XXREAL_0:2;
then W . j5 in W .vertices() by GLIB_001:88;
then W . j5 = v by A1, TARSKI:def 1;
hence contradiction by A3, A6, A5, GLIB_001:def 28; :: 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