let G be _Graph; :: thesis: for e, x being object st e Joins x,x,G holds
G .walkOf (x,e,x) is Cycle-like
let e, x be object ; :: thesis: ( e Joins x,x,G implies G .walkOf (x,e,x) is Cycle-like )
set W = G .walkOf (x,e,x);
assume e Joins x,x,G ; :: thesis: G .walkOf (x,e,x) is Cycle-like
then len (G .walkOf (x,e,x)) = 3 by Th13;
then G .walkOf (x,e,x) is trivial by Lm54;
hence G .walkOf (x,e,x) is Cycle-like ; :: thesis: verum