let G be _finite _Graph; ( card (the_Vertices_of G) <= 3 implies G is chordal )
assume A1:
card (the_Vertices_of G) <= 3
; G is chordal
now 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;
( W .length() > 3 implies not W is Cycle-like )assume that A2:
W .length() > 3
and A3:
W is
Cycle-like
;
contradictionset 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;
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;
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
; verum