theorem Th22: :: GRAPH_5:24

for i being Nat
for G being Graph
for pe being FinSequence of the carrier' of G
for v being Element of G st i in dom pe & ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) holds
v in vertices pe