reconsider fc = c as Subset of c by FINSEQ_6:152;
reconsider fvs = vs as Subset of vs by FINSEQ_6:152;
reconsider sc = c as oriented simple Chain of G by A2, Th19;
take fc ; :: thesis:
take fvs ; :: thesis:
take sc ; :: thesis:
take vs ; :: thesis:
thus ( Seq fc = sc & Seq fvs = vs ) by FINSEQ_3:116; :: thesis:
thus vs is_oriented_vertex_seq_of sc by A1; :: thesis:
thus ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) ) ; :: thesis:

end;

defpred S₁[ Nat] means 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
( Seq fc = c1 & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c1 & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c1 = $1 & not c1 is Simple );
S₁[ len c]

reconsider fc = c as Subset of c by FINSEQ_6:152;
reconsider fvs = vs as Subset of vs by FINSEQ_6:152;
take fc ; :: thesis:
take fvs ; :: thesis:
take c ; :: thesis:
take vs ; :: thesis:
thus ( Seq fc = c & Seq fvs = vs ) by FINSEQ_3:116; :: thesis:
thus vs is_oriented_vertex_seq_of c by A1; :: thesis:
thus ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) ) ; :: thesis:
thus ( len c = len c & not c is Simple ) by A3; :: thesis:

end;

then A4: ex k being Nat st S₁[k] ;
consider k being Nat such that
A5: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A4);
consider fc being Subset of c, fvs being Subset of vs, c1 being oriented Chain of G, vs1 being FinSequence of the carrier of G such that
A6: Seq fc = c1 and
A7: Seq fvs = vs1 and
A8: vs1 is_oriented_vertex_seq_of c1 and
A9: vs . 1 = vs1 . 1 and
A10: vs . (len vs) = vs1 . (len vs1) and
A11: len c1 = k and
A12: not c1 is Simple by A5;
consider fc1 being Subset of c1, fvs1 being Subset of vs1, c2 being oriented Chain of G, vs2 being FinSequence of the carrier of G such that
A13: len c2 < len c1 and
A14: vs2 is_oriented_vertex_seq_of c2 and
len vs2 < len vs1 and
A15: vs1 . 1 = vs2 . 1 and
A16: vs1 . (len vs1) = vs2 . (len vs2) and
A17: Seq fc1 = c2 and
A18: Seq fvs1 = vs2 by A8, A12, Th20;
reconsider fc9 = fc | (rng ((Sgm (dom fc)) | (dom fc1))) as Subset of c by FINSEQ_6:153;
A19: Seq fc9 = c2 by A6, A17, FINSEQ_6:154;
reconsider fvs9 = fvs | (rng ((Sgm (dom fvs)) | (dom fvs1))) as Subset of vs by FINSEQ_6:153;
A20: Seq fvs9 = vs2 by A7, A18, FINSEQ_6:154;

assume c2 is oriented Simple Chain of G ; :: thesis:
then reconsider sc = c2 as oriented simple Chain of G by Th19;
take fc9 = fc9; :: thesis:
take sc = sc; :: thesis:
Seq fc9 = sc by A6, A17, FINSEQ_6:154;
hence ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) by A9, A10, A14, A15, A16, A20; :: thesis:

end;

hence ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) by A5, A9, A10, A11, A13, A14, A15, A16, A19, A20; :: thesis:

end;