let G be Graph; :: thesis: {} is Element of G -CycleSet
reconsider p = {} as Path of G by GRAPH_1:14;
consider v being Vertex of G;
( <*v*> is_vertex_seq_of p & <*v*> . 1 = <*v*> . (len <*v*>) ) by FINSEQ_1:57, GRAPH_2:35;
then p is cyclic by MSSCYC_1:def 2;
hence {} is Element of G -CycleSet by Def8; :: thesis: verum