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

W is chordal ;

hence G is chordal ; :: thesis: verum

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

then
for W being Walk of G st W .length() > 3 & W is Cycle-like 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;

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;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

then A13:
{(W . n1),(W . n2),(W . n3),(W . n4)} c= the_Vertices_of G
;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

end;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 Gend;

hence
x in the_Vertices_of G
; :: thesis: verumper cases
( x = W . n1 or x = W . n2 or x = W . n3 or x = W . n4 )
by A12, ENUMSET1:def 2;

end;

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

W is chordal ;

hence G is chordal ; :: thesis: verum