let G be _Graph; :: thesis: ( G is edgeless implies ( G is acyclic & G is chordal ) )
assume A1: G is edgeless ; :: thesis: ( G is acyclic & G is chordal )
then for W being Walk of G holds not W is Cycle-like ;
hence G is acyclic by GLIB_002:def 2; :: thesis: G is chordal
for W being Walk of G st W .length() > 3 & W is Cycle-like holds
W is chordal by A1;
hence G is chordal by CHORD:def 11; :: thesis: verum