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;
A1: <*v*> is_vertex_seq_of p by GRAPH_2:35;
<*v*> . 1 = <*v*> . (len <*v*>) by FINSEQ_1:57;
then p is cyclic by A1, MSSCYC_1:def 2;
hence {} is Element of G -CycleSet by Def8; :: thesis: verum