theorem Th34: :: GRAPH_2:34

for G being Graph
for vs1, vs2 being FinSequence of the carrier of G
for c being Chain of G st c <> {} & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & vs1 <> vs2 holds
( vs1 . 1 <> vs2 . 1 & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )