let G be Graph; :: thesis: for vs being FinSequence of the carrier of G
for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
vs is_vertex_seq_of c
let vs be FinSequence of the carrier of G; :: thesis: for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
vs is_vertex_seq_of c
let c be oriented Chain of G; :: thesis: ( vs is_oriented_vertex_seq_of c implies vs is_vertex_seq_of c )
assume A1: vs is_oriented_vertex_seq_of c ; :: thesis: vs is_vertex_seq_of c
then A2: len vs = (len c) + 1 ;
for n being Nat st 1 <= n & n <= len c holds
c . n joins vs /. n,vs /. (n + 1) by A1, Th1;
hence vs is_vertex_seq_of c by A2, GRAPH_2:def 6; :: thesis: verum