:: deftheorem Def14 defines Chain GRAPH_1:def 14 :
for G being Graph
for b₂ being FinSequence holds
( b₂ is Chain of G iff ( ( for n being Nat st 1 <= n & n <= len b₂ holds
b₂ . n in the carrier' of G ) & ex p being FinSequence st
( len p = (len b₂) + 1 & ( for n being Nat st 1 <= n & n <= len p holds
p . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len b₂ holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & b₂ . n joins x9,y9 ) ) ) ) );