let G be _Graph; :: thesis: for e, x, y being set holds
( e Joins x,y,G iff (G .walkOf x,e,y) .edgeSeq() = <*e*> )
let e, x, y be set ; :: thesis: ( e Joins x,y,G iff (G .walkOf x,e,y) .edgeSeq() = <*e*> )
set W = G .walkOf x,e,y;

hereby :: thesis: ( (G .walkOf x,e,y) .edgeSeq() = <*e*> implies e Joins x,y,G )

assume A1: e Joins x,y,G ; :: thesis: (G .walkOf x,e,y) .edgeSeq() = <*e*>
then len (G .walkOf x,e,y) = 3 by Th15;
then A2: 2 + 1 = (2 * (len ((G .walkOf x,e,y) .edgeSeq() ))) + 1 by Def15;
A3: G .walkOf x,e,y = <*x,e,y*> by A1, Def5;

A4: now

let k be Nat; :: thesis: ( 1 <= k & k <= len ((G .walkOf x,e,y) .edgeSeq() ) implies ((G .walkOf x,e,y) .edgeSeq() ) . k = <*e*> . k )
assume that
A5: 1 <= k and
A6: k <= len ((G .walkOf x,e,y) .edgeSeq() ) ; :: thesis: ((G .walkOf x,e,y) .edgeSeq() ) . k = <*e*> . k
A7: k = 1 by A2, A5, A6, XXREAL_0:1;
then ((G .walkOf x,e,y) .edgeSeq() ) . k = (G .walkOf x,e,y) . (2 * 1) by A6, Def15
.= e by A3, FINSEQ_1:62 ;
hence ((G .walkOf x,e,y) .edgeSeq() ) . k = <*e*> . k by A7, FINSEQ_1:def 8; :: thesis: verum

end;

len ((G .walkOf x,e,y) .edgeSeq() ) = len <*e*> by A2, FINSEQ_1:56;
hence (G .walkOf x,e,y) .edgeSeq() = <*e*> by A4, FINSEQ_1:18; :: thesis: verum

end;

assume (G .walkOf x,e,y) .edgeSeq() = <*e*> ; :: thesis: e Joins x,y,G
then len ((G .walkOf x,e,y) .edgeSeq() ) = 1 by FINSEQ_1:56;
then A8: len (G .walkOf x,e,y) = (2 * 1) + 1 by Def15;

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 A8, Th14; :: thesis: verum

end;

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