let G be _Graph; :: thesis: for X being set holds G .edgesInto X = union { (v .edgesIn()) where v is Vertex of G : v in X }
let X be set ; :: thesis: G .edgesInto X = union { (v .edgesIn()) where v is Vertex of G : v in X }
set S = { (v .edgesIn()) where v is Vertex of G : v in X } ;

now :: thesis: for e being object holds
( ( e in G .edgesInto X implies e in union { (v .edgesIn()) where v is Vertex of G : v in X } ) & ( e in union { (v .edgesIn()) where v is Vertex of G : v in X } implies e in G .edgesInto X ) )

let e be object ; :: thesis: ( ( e in G .edgesInto X implies e in union { (v .edgesIn()) where v is Vertex of G : v in X } ) & ( e in union { (v .edgesIn()) where v is Vertex of G : v in X } implies e in G .edgesInto X ) )

hereby :: thesis: ( e in union { (v .edgesIn()) where v is Vertex of G : v in X } implies e in G .edgesInto X )

assume e in G .edgesInto X ; :: thesis: e in union { (v .edgesIn()) where v is Vertex of G : v in X }
then A1: ( e in the_Edges_of G & (the_Target_of G) . e in X ) by Def26;
then e Joins (the_Source_of G) . e,(the_Target_of G) . e,G ;
then reconsider v = (the_Target_of G) . e as Vertex of G by FUNCT_2:5;
A2: e in v .edgesIn() by A1, Lm7;
v .edgesIn() in { (v .edgesIn()) where v is Vertex of G : v in X } by A1;
hence e in union { (v .edgesIn()) where v is Vertex of G : v in X } by A2, TARSKI:def 4; :: thesis: verum

end;

assume e in union { (v .edgesIn()) where v is Vertex of G : v in X } ; :: thesis: e in G .edgesInto X
then consider E being set such that
A3: ( e in E & E in { (v .edgesIn()) where v is Vertex of G : v in X } ) by TARSKI:def 4;
consider v being Vertex of G such that
A4: ( E = v .edgesIn() & v in X ) by A3;
( e in the_Edges_of G & (the_Target_of G) . e = v ) by A3, A4, Lm7;
hence e in G .edgesInto X by A4, Def26; :: thesis: verum

end;

hence G .edgesInto X = union { (v .edgesIn()) where v is Vertex of G : v in X } by TARSKI:2; :: thesis: verum