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 ;
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 ;
then ((G .walkOf (x,e,y)) .edgeSeq()) . k = (G .walkOf (x,e,y)) . (2 * 1) by
.= e by ;
hence ((G .walkOf (x,e,y)) .edgeSeq()) . k = <*e*> . k by ; :: thesis: verum
end;
len ((G .walkOf (x,e,y)) .edgeSeq()) = len <*e*> by ;
hence (G .walkOf (x,e,y)) .edgeSeq() = <*e*> by ; :: 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,Gend;
hence e Joins x,y,G ; :: thesis: verum