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

let W be Walk of G; :: thesis: ( W .length() > 3 implies not W is Cycle-like )
assume A2: ( W .length() > 3 & W is Cycle-like ) ; :: thesis: contradiction
reconsider n1 = (2 * 0 ) + 1 as odd Nat ;
reconsider n2 = (2 * 1) + 1 as odd Nat ;
reconsider n3 = (2 * 2) + 1 as odd Nat ;
reconsider n4 = (2 * 3) + 1 as odd Nat ;
set x1 = W . n1;
set x2 = W . n2;
set x3 = W . n3;
set x4 = W . n4;
W .length() >= 3 + 1 by A2, NAT_1:13;
then 2 * (W .length() ) >= 2 * 4 by XREAL_1:66;
then (2 * (W .length() )) + 1 >= 8 + 1 by XREAL_1:9;
then A3: len W >= 9 by GLIB_001:113;
then A4: ( n1 < len W & n2 < len W & n3 < len W & n4 < len W ) by XXREAL_0:2;
A5: W is Path-like by A2;
then A6: W . n1 <> W . n2 by A4, GLIB_001:def 28;
A7: W . n1 <> W . n3 by A4, A5, GLIB_001:def 28;
A8: W . n1 <> W . n4 by A4, A5, GLIB_001:def 28;
A9: W . n2 <> W . n3 by A4, A5, GLIB_001:def 28;
A10: W . n2 <> W . n4 by A4, A5, GLIB_001:def 28;
W . n3 <> W . n4 by A4, A5, GLIB_001:def 28;
then A11: card {(W . n1),(W . n2),(W . n3),(W . n4)} = 4 by A6, A7, A8, A9, A10, CARD_2:78;

now

let x be set ; :: 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

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 A3, GLIB_001:8, 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 A3, GLIB_001:8, 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 A3, GLIB_001:8, 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 A3, GLIB_001:8, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence x in the_Vertices_of G ; :: thesis: verum

end;

then {(W . n1),(W . n2),(W . n3),(W . n4)} c= the_Vertices_of G by TARSKI:def 3;
then 4 <= card (the_Vertices_of G) by A11, NAT_1:44;
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 by Def11; :: thesis: verum