:: deftheorem Def2 defines acyclic GLIB_002:def 2 :
for G being _Graph holds
( G is acyclic iff for W being Walk of G holds not W is Cycle-like );