defpred S₁[ set ] means $1 is cyclic Path of G;
set IT = { p where p is Element of the carrier' of G * : S₁[p] } ;
{ p where p is Element of the carrier' of G * : S₁[p] } is Subset of ( the carrier' of G *) from DOMAIN_1:sch 7();
then for x being set st x in { p where p is Element of the carrier' of G * : S₁[p] } holds
x is FinSequence of the carrier' of G by FINSEQ_1:def 11;
then reconsider IT = { p where p is Element of the carrier' of G * : S₁[p] } as FinSequenceSet of the carrier' of G by FINSEQ_2:def 3;
reconsider p = {} as Path of G by GRAPH_1:14;
set v = the Vertex of G;
( <* the Vertex of G*> is_vertex_seq_of p & <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) ) by FINSEQ_1:40, GRAPH_2:32;
then ( p is Element of the carrier' of G * & p is cyclic ) by FINSEQ_1:def 11, MSSCYC_1:def 2;
then p in IT ;
then reconsider IT = IT as FinSequence-DOMAIN of the carrier' of G ;
take IT ; :: thesis: for x being set holds
( x in IT iff x is cyclic Path of G )
let x be set ; :: thesis: ( x in IT iff x is cyclic Path of G )

hereby :: thesis: ( x is cyclic Path of G implies x in IT )

assume x in IT ; :: thesis: x is cyclic Path of G
then ex p being Element of the carrier' of G * st
( p = x & p is cyclic Path of G ) ;
hence x is cyclic Path of G ; :: thesis: verum

end;

assume A1: x is cyclic Path of G ; :: thesis: x in IT
then x is Element of the carrier' of G * by FINSEQ_1:def 11;
hence x in IT by A1; :: thesis: verum