:: deftheorem defines is_vertex_seq_of GRAPH_2:def 2 :
for G being Graph
for vs being FinSequence of the carrier of G
for c being FinSequence holds
( vs is_vertex_seq_of c iff ( len vs = (len c) + 1 & ( for n being Nat st 1 <= n & n <= len c holds
c . n joins vs /. n,vs /. (n + 1) ) ) );