theorem Th6: :: GRAPHSP:6

for G being Graph
for pe, qe being FinSequence of the carrier' of G
for p being oriented Simple Chain of G st p = pe ^ qe & len pe >= 1 & len qe >= 1 holds
( the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) & the Source of G . (p . 1) <> the Source of G . (qe . 1) )