let G be Graph; :: thesis: {} in 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;
then p is cyclic ;
hence {} in G -CycleSet by Def8; :: thesis: verum