theorem :: GRAPH_1:4

for n being Nat
for G being Graph
for p being Chain of G holds p | (Seg n) is Chain of G by Lm2;