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);
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 Th81;
hence (G .walkOf (x,e,y)) .edges() = {e} by FINSEQ_1:39; :: 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 :: 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 A2, A3, Th12; :: thesis: verum
end;
hence e Joins x,y,G ; :: thesis: verum