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;

W is chordal ;

then the finite trivial _Graph is chordal ;

hence ex b_{1} being _Graph st

( b_{1} is trivial & b_{1} is finite & b_{1} is chordal )
; :: thesis: verum

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

then
for W being Walk of the finite trivial _Graph st W .length() > 3 & W is Cycle-like 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;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

W is chordal ;

then the finite trivial _Graph is chordal ;

hence ex b

( b