:: deftheorem defines oriented-vertex-seq GRAPH_4:def 6 :
for G being Graph
for c being oriented Chain of G st c <> {} holds
for b₃ being FinSequence of the carrier of G holds
( b₃ = oriented-vertex-seq c iff b₃ is_oriented_vertex_seq_of c );