for G being Graph
for vs being FinSequence of the carrier of G
for c being Chain of G st vs is_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex sc being simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )