defpred S1[ set ] means $1 is cyclic Path of G;
set IT = { p where p is Element of the carrier' of G * : S1[p] } ;
{ p where p is Element of the carrier' of G * : S1[p] } is Subset of ( the carrier' of G *) from DOMAIN_1:sch 7();
 then for x being object st x in { p where p is Element of the carrier' of G * : S1[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 * : S1[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;
reconsider IT = IT as FinSequenceSet 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