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 )
assume A1: c = {} ; :: thesis: c is cyclic
consider v being Vertex of G;
A2: <*v*> is_vertex_seq_of c by A1, GRAPH_2:35;
<*v*> . 1 = <*v*> . (len <*v*>) by FINSEQ_1:57;
hence c is cyclic by A2, MSSCYC_1:def 2; :: thesis: verum