let G be finite _Graph; :: thesis: ( card () <= 3 implies G is chordal )
assume A1: card () <= 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 ;
then 2 * () >= 2 * 4 by XREAL_1:64;
then (2 * ()) + 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 ;
n2 < len W by ;
then A7: W . n1 <> W . n2 by ;
A8: n3 < len W by ;
then A9: W . n2 <> W . n3 by ;
A10: W . n3 <> W . n4 by ;
A11: W . n2 <> W . n4 by ;
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:
now :: thesis:
per cases ( x = W . n1 or x = W . n2 or x = W . n3 or x = W . n4 ) by ;
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 ;
then card {(W . n1),(W . n2),(W . n3),(W . n4)} = 4 by ;
then 4 <= card () by ;
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