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

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

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

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

assume e in G .edgesInOut X ; :: thesis: e in union { (v .edgesInOut()) where v is Vertex of G : v in X }
then A1: ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) by Th28;
then A2: e Joins (the_Source_of G) . e,(the_Target_of G) . e,G ;

per cases ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) by A1;

suppose A3: (the_Source_of G) . e in X ; :: thesis: e in union { (v .edgesInOut()) where v is Vertex of G : v in X }

reconsider v = (the_Source_of G) . e as Vertex of G by A2, FUNCT_2:5;
A4: e in v .edgesInOut() by A1, Th61;
v .edgesInOut() in { (v .edgesInOut()) where v is Vertex of G : v in X } by A3;
hence e in union { (v .edgesInOut()) where v is Vertex of G : v in X } by A4, TARSKI:def 4; :: thesis: verum

end;

suppose A5: (the_Target_of G) . e in X ; :: thesis: e in union { (v .edgesInOut()) where v is Vertex of G : v in X }

reconsider v = (the_Target_of G) . e as Vertex of G by A2, FUNCT_2:5;
A6: e in v .edgesInOut() by A1, Th61;
v .edgesInOut() in { (v .edgesInOut()) where v is Vertex of G : v in X } by A5;
hence e in union { (v .edgesInOut()) where v is Vertex of G : v in X } by A6, TARSKI:def 4; :: thesis: verum

end;

end;

end;

assume e in union { (v .edgesInOut()) where v is Vertex of G : v in X } ; :: thesis: e in G .edgesInOut X
then consider E being set such that
A7: ( e in E & E in { (v .edgesInOut()) where v is Vertex of G : v in X } ) by TARSKI:def 4;
consider v being Vertex of G such that
A8: ( E = v .edgesInOut() & v in X ) by A7;
( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) by A7, A8, Th61;
hence e in G .edgesInOut X by A8, Th28; :: thesis: verum

end;

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