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

now

given W2 being Walk of G2 such that A1: W2 is Cycle-like ; :: thesis: contradiction
A2: ( W2 is closed & not W2 is trivial & W2 is Path-like ) by A1;
reconsider W = W2 as Walk of G by GLIB_001:168;
( W is closed & not W is trivial & W is Path-like ) by A2, GLIB_001:177;
then W is Cycle-like by GLIB_001:def 31;
hence contradiction by Def2; :: thesis: verum

end;

hence G2 is acyclic by Def2; :: thesis: verum