set S = { (v .edgesIn()) where v is Vertex of G : v in X } ;
defpred S₁[ object , object ] means ex v being Vertex of G st
( G = v & X = v .edgesIn() );
A2: for x, y1, y2 being object st x in X /\ (the_Vertices_of G) & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
A3: for x being object st x in X /\ (the_Vertices_of G) holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in X /\ (the_Vertices_of G) implies ex y being object st S₁[x,y] )
assume x in X /\ (the_Vertices_of G) ; :: thesis: ex y being object st S₁[x,y]
then reconsider v = x as Vertex of G by XBOOLE_0:def 4;
take v .edgesIn() ; :: thesis: S₁[x,v .edgesIn() ]
take v ; :: thesis: ( x = v & v .edgesIn() = v .edgesIn() )
thus ( x = v & v .edgesIn() = v .edgesIn() ) ; :: thesis: verum

end;

consider f being Function such that
A4: dom f = X /\ (the_Vertices_of G) and
A5: for x being object st x in X /\ (the_Vertices_of G) holds
S₁[x,f . x] from FUNCT_1:sch 2(A2, A3);
A6: rng f is finite by A4, FINSET_1:8;

now :: thesis: for E being object st E in { (v .edgesIn()) where v is Vertex of G : v in X } holds
E in rng f

let E be object ; :: thesis: ( E in { (v .edgesIn()) where v is Vertex of G : v in X } implies E in rng f )
assume E in { (v .edgesIn()) where v is Vertex of G : v in X } ; :: thesis: E in rng f
then consider v being Vertex of G such that
A7: ( E = v .edgesIn() & v in X ) ;
A8: v in X /\ (the_Vertices_of G) by A7, XBOOLE_0:def 4;
then consider v0 being Vertex of G such that
A9: ( v = v0 & f . v = v0 .edgesIn() ) by A5;
thus E in rng f by A4, A7, A8, A9, FUNCT_1:3; :: thesis: verum

end;

then { (v .edgesIn()) where v is Vertex of G : v in X } c= rng f by TARSKI:def 3;
then A10: { (v .edgesIn()) where v is Vertex of G : v in X } is finite by A6;
for E being set st E in { (v .edgesIn()) where v is Vertex of G : v in X } holds
E is finite

proof

let E be set ; :: thesis: ( E in { (v .edgesIn()) where v is Vertex of G : v in X } implies E is finite )
assume E in { (v .edgesIn()) where v is Vertex of G : v in X } ; :: thesis: E is finite
then consider v being Vertex of G such that
A11: ( E = v .edgesIn() & v in X ) ;
thus E is finite by A11, Th25; :: thesis: verum

end;

then union { (v .edgesIn()) where v is Vertex of G : v in X } is finite by A10, FINSET_1:7;
hence G .edgesInto X is finite by GLIB_000:158; :: thesis: verum