:: deftheorem defines vertex-seq GRAPH_2:def 10 :
for G being Graph
for oc being oriented Chain of G st oc <> {} holds
for b₃ being FinSequence of the carrier of G holds
( b₃ = vertex-seq oc iff ( b₃ is_vertex_seq_of oc & b₃ . 1 = the Source of G . (oc . 1) ) );