let G be _Graph; :: thesis: for e, x, y being object holds
( e Joins x,y,G iff (G .walkOf (x,e,y)) .edgeSeq() = <*e*> )
let e, x, y be object ; :: 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 Th13;
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 :: thesis: for k being Nat st 1 <= k & k <= len ((G .walkOf (x,e,y)) .edgeSeq()) holds
((G .walkOf (x,e,y)) .edgeSeq()) . k = <*e*> . k

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 ;
hence ((G .walkOf (x,e,y)) .edgeSeq()) . k = <*e*> . k by A7; :: thesis: verum

end;

len ((G .walkOf (x,e,y)) .edgeSeq()) = len <*e*> by A2, FINSEQ_1:39;
hence (G .walkOf (x,e,y)) .edgeSeq() = <*e*> by A4, FINSEQ_1:14; :: 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:39;
then A8: len (G .walkOf (x,e,y)) = (2 * 1) + 1 by Def15;

now :: thesis: e Joins x,y,G

assume not e Joins x,y,G ; :: thesis: contradiction
then G .walkOf (x,e,y) = G .walkOf the Element of the_Vertices_of G by Def5;
hence contradiction by A8, Th12; :: thesis: verum

end;

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