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 ;
then 2 * () >= 2 * 4 by XREAL_1:64;
then (2 * ()) + 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 ;
A25: ( not t3 = 3 or not t7 = len W ) by A24;
reconsider W7 = W . t7 as Vertex of G by ;
t7 <= len W by ;
then W3 <> W7 by ;
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 ;
hence W is chordal by A23, A26, A27, A25, Th84; :: thesis: verum
end;
hence G is chordal ; :: thesis: verum