let G1 be addVertices of G,V; :: thesis: G1 is acyclic
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: contradiction

per cases ( W1 .vertices() misses V \ (the_Vertices_of G) or not W1 is trivial ) by Th94;

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

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: verum

end;

suppose W1 is trivial ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

end;

end;

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