for G being Graph
for c being Chain of G
for vs being FinSequence of the carrier of G st c is cyclic & vs is_vertex_seq_of c holds
vs . 1 = vs . (len vs) by Lm1;