let G1 be addVertices of G,V; :: thesis:
for W1 being Walk of G1 holds not W1 is Cycle-like

proof

given W1 being Walk of G1 such that A1: W1 is Cycle-like ; :: thesis:

per cases by Th94;

suppose W1 .vertices() misses V \ (the_Vertices_of G) ; :: thesis:

then reconsider P = W1 as Walk of G by Th95;
P is Cycle-like by A1, Th80;
hence contradiction by GLIB_002:def 2; :: thesis:

end;

suppose W1 is V5() ; :: thesis:

hence contradiction by A1; :: thesis:

end;

end;

end;

hence G1 is acyclic by GLIB_002:def 2; :: thesis: