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