let G be _Graph; :: thesis: for e, x being set st e Joins x,x,G holds
G .walkOf x,e,x is Cycle-like
let e, x be set ; :: 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 Th15;
then not G .walkOf x,e,x is trivial by Lm54;
hence G .walkOf x,e,x is Cycle-like by Def31; :: thesis: verum