let G be _Graph; :: thesis: ( G is complete implies G is chordal )

assume A21: G is complete ; :: thesis: G is chordal

assume A21: G is complete ; :: thesis: G is chordal

now :: thesis: for W being Walk of G st W .length() > 3 & W is Cycle-like holds

W is chordal

hence
G is chordal
; :: thesis: verumW is chordal

reconsider t7 = (2 * 3) + 1 as odd Nat ;

reconsider t3 = (2 * 1) + 1 as odd Nat ;

let W be Walk of G; :: thesis: ( W .length() > 3 & W is Cycle-like implies W is chordal )

assume that

A22: W .length() > 3 and

A23: W is Cycle-like ; :: thesis: W is chordal

W .length() >= 3 + 1 by A22, NAT_1:13;

then 2 * (W .length()) >= 2 * 4 by XREAL_1:64;

then (2 * (W .length())) + 1 >= 8 + 1 by XREAL_1:7;

then A24: len W >= 9 by GLIB_001:112;

then reconsider W3 = W . t3 as Vertex of G by GLIB_001:7, XXREAL_0:2;

A25: ( not t3 = 3 or not t7 = len W ) by A24;

reconsider W7 = W . t7 as Vertex of G by A24, GLIB_001:7, XXREAL_0:2;

t7 <= len W by A24, XXREAL_0:2;

then W3 <> W7 by A23, GLIB_001:def 28;

then W3,W7 are_adjacent by A21;

then A26: ex e being object st e Joins W3,W7,G ;

A27: t3 + 2 < t7 ;

t7 <= len W by A24, XXREAL_0:2;

hence W is chordal by A23, A26, A27, A25, Th84; :: thesis: verum

end;reconsider t3 = (2 * 1) + 1 as odd Nat ;

let W be Walk of G; :: thesis: ( W .length() > 3 & W is Cycle-like implies W is chordal )

assume that

A22: W .length() > 3 and

A23: W is Cycle-like ; :: thesis: W is chordal

W .length() >= 3 + 1 by A22, NAT_1:13;

then 2 * (W .length()) >= 2 * 4 by XREAL_1:64;

then (2 * (W .length())) + 1 >= 8 + 1 by XREAL_1:7;

then A24: len W >= 9 by GLIB_001:112;

then reconsider W3 = W . t3 as Vertex of G by GLIB_001:7, XXREAL_0:2;

A25: ( not t3 = 3 or not t7 = len W ) by A24;

reconsider W7 = W . t7 as Vertex of G by A24, GLIB_001:7, XXREAL_0:2;

t7 <= len W by A24, XXREAL_0:2;

then W3 <> W7 by A23, GLIB_001:def 28;

then W3,W7 are_adjacent by A21;

then A26: ex e being object st e Joins W3,W7,G ;

A27: t3 + 2 < t7 ;

t7 <= len W by A24, XXREAL_0:2;

hence W is chordal by A23, A26, A27, A25, Th84; :: thesis: verum