let G be _Graph; :: thesis: for X, Y being set holds G .edgesDBetween (X,Y) = union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) }
let X, Y be set ; :: thesis: G .edgesDBetween (X,Y) = union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) }
set S = { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) } ;

now :: thesis: for e being object holds
( ( e in G .edgesDBetween (X,Y) implies e in union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) } ) & ( e in union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) } implies e in G .edgesDBetween (X,Y) ) )

let e be object ; :: thesis: ( ( e in G .edgesDBetween (X,Y) implies e in union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) } ) & ( e in union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) } implies e in G .edgesDBetween (X,Y) ) )

hereby :: thesis: ( e in union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) } implies e in G .edgesDBetween (X,Y) )

assume e in G .edgesDBetween (X,Y) ; :: thesis: e in union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) }
then e DSJoins X,Y,G by Def31;
then A1: ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) ;
then A2: e DJoins (the_Source_of G) . e,(the_Target_of G) . e,G ;
then e Joins (the_Source_of G) . e,(the_Target_of G) . e,G ;
then reconsider v = (the_Source_of G) . e, w = (the_Target_of G) . e as Vertex of G by FUNCT_2:5;
( e DJoins v,w,G & e is set ) by A2;
then ( e in v .edgesOut() & e in w .edgesIn() ) by Th57, Th59;
then A3: e in (v .edgesOut()) /\ (w .edgesIn()) by XBOOLE_0:def 4;
(v .edgesOut()) /\ (w .edgesIn()) in { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) } by A1;
hence e in union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) } by A3, TARSKI:def 4; :: thesis: verum

end;

assume e in union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) } ; :: thesis: e in G .edgesDBetween (X,Y)
then consider E being set such that
A4: ( e in E & E in { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) } ) by TARSKI:def 4;
consider v, w being Vertex of G such that
A5: ( E = (v .edgesOut()) /\ (w .edgesIn()) & v in X & w in Y ) by A4;
( e in v .edgesOut() & e in w .edgesIn() ) by A4, A5, XBOOLE_0:def 4;
then ( e in the_Edges_of G & (the_Source_of G) . e = v & (the_Target_of G) . e = w ) by Lm7, Lm8;
then e DJoins v,w,G ;
then e DSJoins X,Y,G by A5;
hence e in G .edgesDBetween (X,Y) by Def31; :: thesis: verum

end;

hence G .edgesDBetween (X,Y) = union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) } by TARSKI:2; :: thesis: verum