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 Def31;
then ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) ;
then ( e in G .edgesOutOf X & e in G .edgesInto Y ) by Def26, Def27;
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 Def26, Def27;
then e DSJoins X,Y,G ;
hence e in G .edgesDBetween (X,Y) by Def31; :: thesis: verum

end;

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