let G be _Graph; 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 ; 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 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 ;
( ( 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 ( 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)
;
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 GLIB_000:def 31;
then A1:
(
e in the_Edges_of G &
(the_Source_of G) . e in X &
(the_Target_of G) . e in Y )
by GLIB_000:def 16;
then A2:
e DJoins (the_Source_of G) . e,
(the_Target_of G) . e,
G
by GLIB_000:def 14;
then
e Joins (the_Source_of G) . e,
(the_Target_of G) . e,
G
by GLIB_000:16;
then reconsider v =
(the_Source_of G) . e,
w =
(the_Target_of G) . e as
Vertex of
G by GLIB_000:13;
(
e DJoins v,
w,
G &
e is
set )
by A2, TARSKI:1;
then
(
e in v .edgesOut() &
e in w .edgesIn() )
by GLIB_000:57, GLIB_000:59;
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;
verum
end; assume
e in union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) }
;
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 GLIB_000:56, GLIB_000:58;
then
e DJoins v,
w,
G
by GLIB_000:def 14;
then
e DSJoins X,
Y,
G
by A5, GLIB_009:7;
hence
e in G .edgesDBetween (
X,
Y)
by GLIB_000:def 31;
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; verum