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 & the Source of G . (p . 1) <> the Target of G . (p . (len p)) holds
( not the Source of G . (p . 1) in vertices qe & not the Target of G . (p . (len p)) in vertices pe )