let G be _Graph; :: thesis: for e, x, y being set holds
( e Joins x,y,G iff (G .walkOf x,e,y) .edges() = {e} )
let e, x, y be set ; :: thesis: ( e Joins x,y,G iff (G .walkOf x,e,y) .edges() = {e} )
set W = G .walkOf x,e,y;

hereby :: thesis: ( (G .walkOf x,e,y) .edges() = {e} implies e Joins x,y,G )

assume e Joins x,y,G ; :: thesis: (G .walkOf x,e,y) .edges() = {e}
then (G .walkOf x,e,y) .edgeSeq() = <*e*> by Th84;
hence (G .walkOf x,e,y) .edges() = {e} by FINSEQ_1:56; :: thesis: verum

end;

assume (G .walkOf x,e,y) .edges() = {e} ; :: thesis: e Joins x,y,G
then e in (G .walkOf x,e,y) .edges() by TARSKI:def 1;
then consider n being even Element of NAT such that
A1: 1 <= n and
A2: n <= len (G .walkOf x,e,y) and
(G .walkOf x,e,y) . n = e by Lm46;
A3: (2 * 0 ) + 1 < n by A1, XXREAL_0:1;

now

assume not e Joins x,y,G ; :: thesis: contradiction
then G .walkOf x,e,y = G .walkOf (choose (the_Vertices_of G)) by Def5;
hence contradiction by A2, A3, Th14; :: thesis: verum

end;

hence e Joins x,y,G ; :: thesis: verum