set S = { (v .edgesOut()) where v is Vertex of G : v in X } ;
defpred S1[ object , object ] means ex v being Vertex of G st
( G = v & X = v .edgesOut() );
A12: for x, y1, y2 being object st x in X /\ (the_Vertices_of G) & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
A13: for x being object st x in X /\ (the_Vertices_of G) holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in X /\ (the_Vertices_of G) implies ex y being object st S1[x,y] )
assume x in X /\ (the_Vertices_of G) ; :: thesis: ex y being object st S1[x,y]
then reconsider v = x as Vertex of G by XBOOLE_0:def 4;
take v .edgesOut() ; :: thesis: S1[x,v .edgesOut() ]
take v ; :: thesis: ( x = v & v .edgesOut() = v .edgesOut() )
thus ( x = v & v .edgesOut() = v .edgesOut() ) ; :: thesis: verum
end;
consider f being Function such that
A14: dom f = X /\ (the_Vertices_of G) and
A15: for x being object st x in X /\ (the_Vertices_of G) holds
S1[x,f . x] from FUNCT_1:sch 2(A12, A13);
 A16: rng f is finite by A14, FINSET_1:8;
now :: thesis: for E being object st E in { (v .edgesOut()) where v is Vertex of G : v in X } holds
E in rng f
let E be object ; :: thesis: ( E in { (v .edgesOut()) where v is Vertex of G : v in X } implies E in rng f )
assume E in { (v .edgesOut()) where v is Vertex of G : v in X } ; :: thesis: E in rng f
then consider v being Vertex of G such that
A17: ( E = v .edgesOut() & v in X ) ;
A18: v in X /\ (the_Vertices_of G) by A17, XBOOLE_0:def 4;
then consider v0 being Vertex of G such that
A19: ( v = v0 & f . v = v0 .edgesOut() ) by A15;
thus E in rng f by A14, A17, A18, A19, FUNCT_1:3; :: thesis: verum
end;
then { (v .edgesOut()) where v is Vertex of G : v in X } c= rng f by TARSKI:def 3;
then A20: { (v .edgesOut()) where v is Vertex of G : v in X } is finite by A16;
for E being set st E in { (v .edgesOut()) where v is Vertex of G : v in X } holds
E is finite
proof
let E be set ; :: thesis: ( E in { (v .edgesOut()) where v is Vertex of G : v in X } implies E is finite )
assume E in { (v .edgesOut()) where v is Vertex of G : v in X } ; :: thesis: E is finite
then consider v being Vertex of G such that
A21: ( E = v .edgesOut() & v in X ) ;
thus E is finite by A21, Th25; :: thesis: verum
end;
then union { (v .edgesOut()) where v is Vertex of G : v in X } is finite by A20, FINSET_1:7;
hence G .edgesOutOf X is finite by GLIBPRE0:37; :: thesis: verum