set V = the_Vertices_of G;
set S = { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } ;
defpred S1[ object , object ] means ex v, w being Vertex of G st
( G = [v,w] & X = (v .edgesInOut()) /\ (w .edgesInOut()) );
A22: for x, y1, y2 being object st x in [:X,Y:] /\ [:(the_Vertices_of G),(the_Vertices_of G):] & S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x, y1, y2 be object ; :: thesis: ( x in [:X,Y:] /\ [:(the_Vertices_of G),(the_Vertices_of G):] & S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume A23: ( x in [:X,Y:] /\ [:(the_Vertices_of G),(the_Vertices_of G):] & S1[x,y1] & S1[x,y2] ) ; :: thesis: y1 = y2
then consider v1, w1 being Vertex of G such that
A24: ( x = [v1,w1] & y1 = (v1 .edgesInOut()) /\ (w1 .edgesInOut()) ) ;
consider v2, w2 being Vertex of G such that
A25: ( x = [v2,w2] & y2 = (v2 .edgesInOut()) /\ (w2 .edgesInOut()) ) by A23;
( v1 = v2 & w1 = w2 ) by A24, A25, XTUPLE_0:1;
hence y1 = y2 by A24, A25; :: thesis: verum
end;
A26: for x being object st x in [:X,Y:] /\ [:(the_Vertices_of G),(the_Vertices_of G):] holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in [:X,Y:] /\ [:(the_Vertices_of G),(the_Vertices_of G):] implies ex y being object st S1[x,y] )
assume A27: x in [:X,Y:] /\ [:(the_Vertices_of G),(the_Vertices_of G):] ; :: thesis: ex y being object st S1[x,y]
then x in [:X,Y:] by XBOOLE_0:def 4;
then consider v, w being object such that
A28: ( v in X & w in Y & x = [v,w] ) by ZFMISC_1:def 2;
x in [:(the_Vertices_of G),(the_Vertices_of G):] by A27, XBOOLE_0:def 4;
then consider v9, w9 being object such that
A29: ( v9 in the_Vertices_of G & w9 in the_Vertices_of G & x = [v9,w9] ) by ZFMISC_1:def 2;
reconsider v = v, w = w as Vertex of G by A28, A29, XTUPLE_0:1;
take (v .edgesInOut()) /\ (w .edgesInOut()) ; :: thesis: S1[x,(v .edgesInOut()) /\ (w .edgesInOut())]
take v ; :: thesis: ex w being Vertex of G st
( x = [v,w] & (v .edgesInOut()) /\ (w .edgesInOut()) = (v .edgesInOut()) /\ (w .edgesInOut()) )
take w ; :: thesis: ( x = [v,w] & (v .edgesInOut()) /\ (w .edgesInOut()) = (v .edgesInOut()) /\ (w .edgesInOut()) )
thus ( x = [v,w] & (v .edgesInOut()) /\ (w .edgesInOut()) = (v .edgesInOut()) /\ (w .edgesInOut()) ) by A28; :: thesis: verum
end;
consider f being Function such that
A30: dom f = [:X,Y:] /\ [:(the_Vertices_of G),(the_Vertices_of G):] and
A31: for x being object st x in [:X,Y:] /\ [:(the_Vertices_of G),(the_Vertices_of G):] holds
S1[x,f . x] from FUNCT_1:sch 2(A22, A26);
 A32: rng f is finite by A30, FINSET_1:8;
now :: thesis: for E being object st E in { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } holds
E in rng f
let E be object ; :: thesis: ( E in { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } implies E in rng f )
assume E in { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } ; :: thesis: E in rng f
then consider v, w being Vertex of G such that
A33: ( E = (v .edgesInOut()) /\ (w .edgesInOut()) & v in X & w in Y ) ;
A34: [v,w] in [:X,Y:] by A33, ZFMISC_1:def 2;
[v,w] in [:(the_Vertices_of G),(the_Vertices_of G):] by ZFMISC_1:def 2;
then A35: [v,w] in [:X,Y:] /\ [:(the_Vertices_of G),(the_Vertices_of G):] by A34, XBOOLE_0:def 4;
then consider v0, w0 being Vertex of G such that
A36: ( [v,w] = [v0,w0] & f . [v,w] = (v0 .edgesInOut()) /\ (w0 .edgesInOut()) ) by A31;
( v = v0 & w = w0 ) by A36, XTUPLE_0:1;
hence E in rng f by A30, A33, A35, A36, FUNCT_1:3; :: thesis: verum
end;
then { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } c= rng f by TARSKI:def 3;
then A37: { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } is finite by A32;
for E being set st E in { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } holds
E is finite
proof
let E be set ; :: thesis: ( E in { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } implies E is finite )
assume E in { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } ; :: thesis: E is finite
then consider v, w being Vertex of G such that
A38: ( E = (v .edgesInOut()) /\ (w .edgesInOut()) & v in X & w in Y ) ;
thus E is finite by A38; :: thesis: verum
end;
then A39: union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } is finite by A37, FINSET_1:7;
G .edgesBetween (X,Y) c= union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) } by GLIBPRE0:40;
hence G .edgesBetween (X,Y) is finite by A39; :: thesis: verum