let G be Graph; :: thesis: {} is Element of G -CycleSet
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 cyclic by MSSCYC_1:def 2;
hence {} is Element of G -CycleSet by Def8; :: thesis: verum