:: deftheorem Def7 defines Cycle-like GLPACY00:def 7 :
for F being Graph-yielding Function holds
( F is Cycle-like iff for x being object st x in dom F holds
ex G being _Graph st
( F . x = G & G is Cycle-like ) );