theorem Th20: :: GRAPH_4:20

for G being Graph
for vs being FinSequence of the carrier of G
for c being oriented Chain of G st not c is Simple & vs is_oriented_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )