let G be _Graph; :: thesis: ( G is complete implies 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

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;

hence G is chordal ; :: thesis: verum