let G2 be Subgraph of G; :: thesis: G2 is acyclic

now :: thesis: for W2 being Walk of G2 holds not W2 is Cycle-like

hence
G2 is acyclic
; :: thesis: verumgiven W2 being Walk of G2 such that A1:
W2 is Cycle-like
; :: thesis: contradiction

reconsider W = W2 as Walk of G by GLIB_001:167;

A2: W is Path-like by A1, GLIB_001:176;

( W is closed & not W is trivial ) by A1, GLIB_001:176;

then W is Cycle-like by A2, GLIB_001:def 31;

hence contradiction by Def2; :: thesis: verum

end;reconsider W = W2 as Walk of G by GLIB_001:167;

A2: W is Path-like by A1, GLIB_001:176;

( W is closed & not W is trivial ) by A1, GLIB_001:176;

then W is Cycle-like by A2, GLIB_001:def 31;

hence contradiction by Def2; :: thesis: verum