set G = the _finite _trivial _Graph;
consider v being Vertex of the _finite _trivial _Graph such that
A1: the_Vertices_of the _finite _trivial _Graph = {v} by GLIB_000:22;

now :: thesis: for W being Walk of the _finite _trivial _Graph st W .length() > 3 holds
not W is Cycle-like

reconsider j5 = (2 * 2) + 1 as odd Nat ;
reconsider j3 = (2 * 1) + 1 as odd Nat ;
let W be Walk of the _finite _trivial _Graph; :: 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:68;
then (2 * (W .length())) + 1 > 6 + 1 by XREAL_1:8;
then A4: len W > 7 by GLIB_001:112;
then j3 <= len W by XXREAL_0:2;
then W . j3 in W .vertices() by GLIB_001:87;
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:87;
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 the _finite _trivial _Graph st W .length() > 3 & W is Cycle-like holds
W is chordal ;
then the _finite _trivial _Graph is chordal ;
hence ex b₁ being _Graph st
( b₁ is _trivial & b₁ is _finite & b₁ is chordal ) ; :: thesis: verum