:: deftheorem defines cyclic MSSCYC_1:def 2 :
for G being Graph
for IT being Chain of G holds
( IT is cyclic iff ex p being FinSequence of the carrier of G st
( p is_vertex_seq_of IT & p . 1 = p . (len p) ) );