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

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

given 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 & 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;

hence G2 is acyclic ; :: thesis: verum