theorem Th25: :: GRAPH_5:27

for G being Graph
for pe being FinSequence of the carrier' of G
for p, q being oriented Chain of G st p = q ^ pe & len q >= 1 & len pe = 1 holds
vertices p = (vertices q) \/ {( the Target of G . (pe . 1))}