:: deftheorem defines Circuit-like GLIB_001:def 30 :
for G being _Graph
for W being Walk of G holds
( W is Circuit-like iff ( W is closed & W is Trail-like & W is V5() ) );