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 not G .walkOf (x,e,x) is trivial by Lm54;

hence G .walkOf (x,e,x) is Cycle-like ; :: thesis: verum

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 not G .walkOf (x,e,x) is trivial by Lm54;

hence G .walkOf (x,e,x) is Cycle-like ; :: thesis: verum