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

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

let e be object ; :: thesis: ( e in G .edgesBetween (X,Y) implies e in union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } )
assume e in G .edgesBetween (X,Y) ; :: thesis: e in union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) }
then e SJoins X,Y,G by Def30;
then A1: ( e in the_Edges_of G & ( ( (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) or ( (the_Source_of G) . e in Y & (the_Target_of G) . e in X ) ) ) ;
then A2: 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 Joins v,w,G & e Joins w,v,G & e is set ) by A2;
then ( e in v .edgesInOut() & e in w .edgesInOut() ) by Th64;
then A3: e in (v .edgesInOut()) /\ (w .edgesInOut()) by XBOOLE_0:def 4;
(v .edgesInOut()) /\ (w .edgesInOut()) in { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } by A1;
hence e in union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } by A3, TARSKI:def 4; :: thesis: verum

end;

hence G .edgesBetween (X,Y) c= union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } ; :: thesis: verum