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 V5() ) 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