let G be Graph; :: thesis: for c being Chain of G st c = {} holds
c is cyclic
let c be Chain of G; :: thesis: ( c = {} implies c is cyclic )
consider v being Vertex of G;
assume c = {} ; :: thesis: c is cyclic
then A1: <*v*> is_vertex_seq_of c by GRAPH_2:35;
<*v*> . 1 = <*v*> . (len <*v*>) by FINSEQ_1:57;
hence c is cyclic by A1, MSSCYC_1:def 2; :: thesis: verum