for G being connected _Graph st ex v1, v2 being Vertex of G ex e being object ex H being addEdge of G,v1,e,v2 st
( not e in the_Edges_of G & ( for W1, W2 being Walk of H st W1 is Cycle-like & W2 is Cycle-like holds
W1 .edges() = W2 .edges() ) ) holds
G is Tree-like