let C be _Graph; :: thesis: ( C is 3 -vertex & C is Cycle-like implies ( C is simple & C is complete & C is chordal ) )
assume A2: ( C is 3 -vertex & C is Cycle-like ) ; :: thesis: ( C is simple & C is complete & C is chordal )
then ( C is 0 + 3 -vertex & C is Cycle-like ) ;
hence A3: C is simple ; :: thesis: ( C is complete & C is chordal )

now :: thesis: for v, w being Vertex of C st v <> w holds
v,w are_adjacent

let v, w be Vertex of C; :: thesis: ( v <> w implies v,w are_adjacent )
assume A4: v <> w ; :: thesis: v,w are_adjacent
2 = v .degree() by A2, GLIB_016:def 4
.= card (v .allNeighbors()) by A3, GLIB_000:111 ;
then consider x, y being object such that
A5: ( x <> y & v .allNeighbors() = {x,y} ) by CARD_2:60;
( w = x or w = y )

proof

assume A6: ( w <> x & w <> y ) ; :: thesis: contradiction
A7: v .allNeighbors() c= (the_Vertices_of C) \ {v} by A3, GLIB_000:175;
v in {v} by TARSKI:def 1;
then not v in v .allNeighbors() by A7, XBOOLE_0:def 5;
then A8: ( v <> x & v <> y ) by A5, TARSKI:def 2;
{v,w} \/ {x,y} c= the_Vertices_of C by A5, XBOOLE_1:8;
then {v,w,x,y} c= the_Vertices_of C by ENUMSET1:5;
then card {v,w,x,y} c= C .order() by CARD_1:11;
then 4 c= C .order() by A4, A5, A6, A8, CARD_2:59;
then Segm 4 c= Segm 3 by A2, GLIB_013:def 3;
hence contradiction by NAT_1:39; :: thesis: verum

end;

then w in v .allNeighbors() by A5, TARSKI:def 2;
then ex e being object st e Joins v,w,C by GLIB_000:71;
hence v,w are_adjacent by CHORD:def 3; :: thesis: verum

end;

hence C is complete by CHORD:def 6; :: thesis: C is chordal

now :: thesis: for P being Walk of C st P .length() > 3 & P is Cycle-like holds
P is chordal

let P be Walk of C; :: thesis: ( P .length() > 3 & P is Cycle-like implies P is chordal )
assume A9: ( P .length() > 3 & P is Cycle-like ) ; :: thesis: P is chordal
then A10: 3 in Segm (P .length()) by NAT_1:44;
P .length() c= C .order() by A9, GLIBPRE1:26;
then P .length() c= 3 by A2, GLIB_013:def 3;
then 3 in 3 by A10;
hence P is chordal ; :: thesis: verum

end;

hence C is chordal by CHORD:def 11; :: thesis: verum