:: deftheorem defines is_cycle_of SGRAPH1:def 11 :
for X being set
for g being SimpleGraph of X
for p being set holds
( p is_cycle_of g iff ex v being Element of the carrier of g st p in PATHS (v,v) );