theorem :: GLIB_001:156
for G being _Graph
for e, x being object st e Joins x,x,G holds
G .walkOf (x,e,x) is Cycle-like