for G being Graph
for v1, v2 being Vertex of G
for c being Chain of G
for vs being FinSequence of the carrier of G
for vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) st vs9 = vs & vs is_vertex_seq_of c holds
vs9 is_vertex_seq_of c