set W = G .walkOf (x,e,x);

now

per cases ( e Joins x,x,G or not e Joins x,x,G ) ;

suppose A1: e Joins x,x,G ; :: thesis: G .walkOf (x,e,x) is closed

then A2: (G .walkOf (x,e,x)) .last() = x by Lm6;
(G .walkOf (x,e,x)) .first() = x by A1, Lm6;
hence G .walkOf (x,e,x) is closed by A2, Def24; :: thesis: verum

end;

suppose not e Joins x,x,G ; :: thesis: G .walkOf (x,e,x) is closed

then G .walkOf (x,e,x) = G .walkOf (choose (the_Vertices_of G)) by Def5;
hence G .walkOf (x,e,x) is closed ; :: thesis: verum

end;

end;

end;

hence G .walkOf (x,e,x) is closed ; :: thesis: verum