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 * () > 2 * 3 by ;
then (2 * ()) + 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 ;
A6: j5 <= len W by ;
then W . j5 in W .vertices() by GLIB_001:87;
then W . j5 = v by ;
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 b1 being _Graph st
( b1 is trivial & b1 is finite & b1 is chordal ) ; :: thesis: verum