let C be _Graph; :: thesis: ( C is n + 4 -vertex & C is Cycle-like implies ( not C is chordal & not C is complete ) )
assume A1: ( C is n + 4 -vertex & C is Cycle-like ) ; :: thesis: ( not C is chordal & not C is complete )
ex P being Walk of C st
( P .length() > 3 & P is Cycle-like & not P is chordal )

proof

consider P being Walk of C such that
A2: P is Cycle-like by A1, GLIB_002:def 2;
reconsider P = P as Path of C by A2;
take P ; :: thesis: ( P .length() > 3 & P is Cycle-like & not P is chordal )
A3: P .length() = card (P .edges()) by Th4
.= C .size() by A1, A2, Th39
.= C .order() by A1, Th40
.= n + 4 by A1, GLIB_013:def 3 ;
(n + 1) + 3 > 0 + 3 by XREAL_1:8;
hence P .length() > 3 by A3; :: thesis: ( P is Cycle-like & not P is chordal )

now :: thesis: for m, n being odd Nat st m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,C holds
ex e being object st
( e in P .edges() & e Joins P . m,P . n,C )

let m, n be odd Nat; :: thesis: ( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,C implies ex e being object st
( e in P .edges() & e Joins P . m,P . n,C ) )
assume ( m + 2 < n & n <= len P & P . m <> P . n ) ; :: thesis: ( ex e being object st e Joins P . m,P . n,C implies ex e being object st
( e in P .edges() & e Joins P . m,P . n,C ) )
given e being object such that A4: e Joins P . m,P . n,C ; :: thesis: ex e being object st
( e in P .edges() & e Joins P . m,P . n,C )
take e = e; :: thesis: ( e in P .edges() & e Joins P . m,P . n,C )
e in the_Edges_of C by A4, GLIB_000:def 13;
hence e in P .edges() by A1, A2, Th39; :: thesis: e Joins P . m,P . n,C
thus e Joins P . m,P . n,C by A4; :: thesis: verum

end;

hence ( P is Cycle-like & not P is chordal ) by A2, CHORD:def 10; :: thesis: verum

end;

hence ( not C is chordal & not C is complete ) by CHORD:def 11; :: thesis: verum