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 GLIB_000:64;
consider w2 being Vertex of G such that
A6: e Joins w,w2,G by A4, GLIB_000:64;
A7: ( ( v = w & v2 = w2 ) or ( v = w2 & v2 = w ) ) by A5, A6, GLIB_000:15;
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, GLIB_000:17;
hence e in G .edgesBetween (X,Y) by GLIB_000:def 30; :: 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) by TARSKI:def 3;
G .edgesBetween (X,Y) c= union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } by Th44;
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