for G being Graph
for v1, v2 being Vertex of G
for vs being FinSequence of the carrier of G
for p9 being Path of AddNewEdge (v1,v2)
for vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) st not the carrier' of G in rng p9 & vs = vs9 & vs9 is_vertex_seq_of p9 holds
vs is_vertex_seq_of p9