let G be _Graph; :: thesis:
let X, Y be set ; :: thesis:

now :: thesis:

let e be object ; :: thesis:

hereby :: thesis:

assume e in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose e in G .edgesDBetween (X,Y) ; :: thesis:

then e DSJoins X,Y,G by GLIB_000:def 31;
hence e SJoins X,Y,G by GLIB_009:11; :: thesis:

end;

suppose e in G .edgesDBetween (Y,X) ; :: thesis:

then e DSJoins Y,X,G by GLIB_000:def 31;
hence e SJoins X,Y,G by GLIB_009:11; :: thesis:

end;

end;

end;

assume e SJoins X,Y,G ; :: thesis:

per cases by GLIB_009:11;

suppose e DSJoins X,Y,G ; :: thesis:

then e in G .edgesDBetween (X,Y) by GLIB_000:def 31;
hence e in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) by XBOOLE_0:def 3; :: thesis:

end;

suppose e DSJoins Y,X,G ; :: thesis:

then e in G .edgesDBetween (Y,X) by GLIB_000:def 31;
hence e in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

hence G .edgesBetween (X,Y) = (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) by GLIB_000:def 30; :: thesis: