theorem :: GRAPH_2:50

for p being FinSequence
for n being Nat
for G being Graph st p is Path of G holds
p | (Seg n) is Path of G