theorem :: GRAPH_3:38

for G being Graph
for v1, v2 being Vertex of G
for p being Path of G holds p is Path of AddNewEdge (v1,v2) by Th37;