let G be _Graph; :: thesis: for X, Y being set holds G .edgesDBetween (X,Y) = (G .edgesOutOf X) /\ (G .edgesInto Y)
let X, Y be set ; :: thesis: G .edgesDBetween (X,Y) = (G .edgesOutOf X) /\ (G .edgesInto Y)

now :: thesis: for e being object holds
( ( e in G .edgesDBetween (X,Y) implies e in (G .edgesOutOf X) /\ (G .edgesInto Y) ) & ( e in (G .edgesOutOf X) /\ (G .edgesInto Y) implies e in G .edgesDBetween (X,Y) ) )

let e be object ; :: thesis: ( ( e in G .edgesDBetween (X,Y) implies e in (G .edgesOutOf X) /\ (G .edgesInto Y) ) & ( e in (G .edgesOutOf X) /\ (G .edgesInto Y) implies e in G .edgesDBetween (X,Y) ) )

hereby :: thesis: ( e in (G .edgesOutOf X) /\ (G .edgesInto Y) implies e in G .edgesDBetween (X,Y) )

assume e in G .edgesDBetween (X,Y) ; :: thesis: e in (G .edgesOutOf X) /\ (G .edgesInto Y)
then e DSJoins X,Y,G by GLIB_000:def 31;
then ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) by GLIB_000:def 16;
then ( e in G .edgesOutOf X & e in G .edgesInto Y ) by GLIB_000:def 26, GLIB_000:def 27;
hence e in (G .edgesOutOf X) /\ (G .edgesInto Y) by XBOOLE_0:def 4; :: thesis: verum

end;

assume e in (G .edgesOutOf X) /\ (G .edgesInto Y) ; :: thesis: e in G .edgesDBetween (X,Y)
then ( e in G .edgesOutOf X & e in G .edgesInto Y ) by XBOOLE_0:def 4;
then ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) by GLIB_000:def 26, GLIB_000:def 27;
then e DSJoins X,Y,G by GLIB_000:def 16;
hence e in G .edgesDBetween (X,Y) by GLIB_000:def 31; :: thesis: verum

end;

hence G .edgesDBetween (X,Y) = (G .edgesOutOf X) /\ (G .edgesInto Y) by TARSKI:2; :: thesis: verum