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