let G be _Graph; :: thesis: for X, Y being set st X misses Y holds
G .edgesBetween (X,Y) = union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) }
let X, Y be set ; :: thesis: ( X misses Y implies G .edgesBetween (X,Y) = union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } )
assume A1: X misses Y ; :: thesis: G .edgesBetween (X,Y) = 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 union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } holds
e in G .edgesBetween (X,Y)

let e be object ; :: thesis: ( e in union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } implies e in G .edgesBetween (X,Y) )
assume e in union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } ; :: thesis: e in G .edgesBetween (X,Y)
then consider E being set such that
A2: ( e in E & E in { ((v .edgesInOut()) /\ (w .edgesInOut())) 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
A3: ( E = (v .edgesInOut()) /\ (w .edgesInOut()) & v in X & w in Y ) by A2;
A4: ( e in v .edgesInOut() & e in w .edgesInOut() ) by A2, A3, XBOOLE_0:def 4;
then consider v2 being Vertex of G such that
A5: e Joins v,v2,G by Th64;
consider w2 being Vertex of G such that
A6: e Joins w,w2,G by A4, Th64;
A7: ( ( v = w & v2 = w2 ) or ( v = w2 & v2 = w ) ) by A5, A6;
v <> w

proof

assume v = w ; :: thesis: contradiction
then v in X /\ Y by A3, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum

end;

then e SJoins X,Y,G by A3, A5, A7;
hence e in G .edgesBetween (X,Y) by Def30; :: thesis: verum

end;

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