let G be _Graph; 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 ; ( 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
; 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 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 ;
( 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 ) }
;
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
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;
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; verum