let G be _finite _Graph; :: thesis: ( card (the_Vertices_of G) <= 3 implies G is chordal )
assume A1: card (the_Vertices_of G) <= 3 ; :: thesis: G is chordal

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

reconsider n4 = (2 * 3) + 1 as odd Nat ;
reconsider n3 = (2 * 2) + 1 as odd Nat ;
reconsider n2 = (2 * 1) + 1 as odd Nat ;
reconsider n1 = (2 * 0) + 1 as odd Nat ;
let W be Walk of G; :: thesis: ( W .length() > 3 implies not W is Cycle-like )
assume that
A2: W .length() > 3 and
A3: W is Cycle-like ; :: thesis: contradiction
set x3 = W . n3;
set x2 = W . n2;
set x4 = W . n4;
set x1 = W . n1;
W .length() >= 3 + 1 by A2, 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 A4: len W >= 9 by GLIB_001:112;
then A5: n4 < len W by XXREAL_0:2;
then A6: W . n1 <> W . n4 by A3, GLIB_001:def 28;
n2 < len W by A4, XXREAL_0:2;
then A7: W . n1 <> W . n2 by A3, GLIB_001:def 28;
A8: n3 < len W by A4, XXREAL_0:2;
then A9: W . n2 <> W . n3 by A3, GLIB_001:def 28;
A10: W . n3 <> W . n4 by A3, A5, GLIB_001:def 28;
A11: W . n2 <> W . n4 by A3, A5, GLIB_001:def 28;

now :: thesis: for x being object st x in {(W . n1),(W . n2),(W . n3),(W . n4)} holds
x in the_Vertices_of G

let x be object ; :: thesis: ( x in {(W . n1),(W . n2),(W . n3),(W . n4)} implies x in the_Vertices_of G )
assume A12: x in {(W . n1),(W . n2),(W . n3),(W . n4)} ; :: thesis: x in the_Vertices_of G

now :: thesis: x in the_Vertices_of G

per cases ( x = W . n1 or x = W . n2 or x = W . n3 or x = W . n4 ) by A12, ENUMSET1:def 2;

suppose x = W . n1 ; :: thesis: x in the_Vertices_of G

hence x in the_Vertices_of G by A4, GLIB_001:7, XXREAL_0:2; :: thesis: verum

end;

suppose x = W . n2 ; :: thesis: x in the_Vertices_of G

hence x in the_Vertices_of G by A4, GLIB_001:7, XXREAL_0:2; :: thesis: verum

end;

suppose x = W . n3 ; :: thesis: x in the_Vertices_of G

hence x in the_Vertices_of G by A4, GLIB_001:7, XXREAL_0:2; :: thesis: verum

end;

suppose x = W . n4 ; :: thesis: x in the_Vertices_of G

hence x in the_Vertices_of G by A4, GLIB_001:7, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence x in the_Vertices_of G ; :: thesis: verum

end;

then A13: {(W . n1),(W . n2),(W . n3),(W . n4)} c= the_Vertices_of G ;
W . n1 <> W . n3 by A3, A8, GLIB_001:def 28;
then card {(W . n1),(W . n2),(W . n3),(W . n4)} = 4 by A7, A6, A9, A11, A10, CARD_2:59;
then 4 <= card (the_Vertices_of G) by A13, NAT_1:43;
hence contradiction by A1, XXREAL_0:2; :: thesis: verum

end;

then for W being Walk of G st W .length() > 3 & W is Cycle-like holds
W is chordal ;
hence G is chordal ; :: thesis: verum