set W = G .walkOf (x,e,x);
now :: thesis: G .walkOf (x,e,x) is closed
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; :: 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 the Element of 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