theorem Th26: :: GRAPH_5:28

for G being Graph
for v being Element of G
for p being oriented Chain of G st v <> the Source of G . (p . 1) & v in vertices p holds
ex i being Nat st
( 1 <= i & i <= len p & v = the Target of G . (p . i) )