let G be _Graph; :: thesis: for e, x, y being object holds

( e Joins x,y,G iff (G .walkOf (x,e,y)) .edges() = {e} )

let e, x, y be object ; :: thesis: ( e Joins x,y,G iff (G .walkOf (x,e,y)) .edges() = {e} )

set W = G .walkOf (x,e,y);

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;

( e Joins x,y,G iff (G .walkOf (x,e,y)) .edges() = {e} )

let e, x, y be object ; :: 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
(G .walkOf (x,e,y)) .edges() = {e}
; :: thesis: e Joins x,y,Gassume
e Joins x,y,G
; :: thesis: (G .walkOf (x,e,y)) .edges() = {e}

then (G .walkOf (x,e,y)) .edgeSeq() = <*e*> by Th81;

hence (G .walkOf (x,e,y)) .edges() = {e} by FINSEQ_1:39; :: thesis: verum

end;then (G .walkOf (x,e,y)) .edgeSeq() = <*e*> by Th81;

hence (G .walkOf (x,e,y)) .edges() = {e} by FINSEQ_1:39; :: thesis: verum

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 :: thesis: e Joins x,y,G

hence
e Joins x,y,G
; :: thesis: verumassume
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 A2, A3, Th12; :: thesis: verum

end;then G .walkOf (x,e,y) = G .walkOf the Element of the_Vertices_of G by Def5;

hence contradiction by A2, A3, Th12; :: thesis: verum