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 )
set v = the Vertex of G;
assume c = {} ; :: thesis: c is cyclic
then A1: <* the Vertex of G*> is_vertex_seq_of c by GRAPH_2:32;
<* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) by FINSEQ_1:40;
hence c is cyclic by A1; :: thesis: verum