:: deftheorem defines cyclic GRAPH_1:def 17 :
for G being Graph
for IT being Path of G holds
( IT is cyclic iff ex p being FinSequence st
( len p = (len IT) + 1 & ( for n being Nat st 1 <= n & n <= len p holds
p . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len IT holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & IT . n joins x9,y9 ) ) & p . 1 = p . (len p) ) );