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

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

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

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

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

end;

assume e in union { (v .edgesOut()) where v is Vertex of G : v in X } ; :: thesis: e in G .edgesOutOf X
then consider E being set such that
A3: ( e in E & E in { (v .edgesOut()) where v is Vertex of G : v in X } ) by TARSKI:def 4;
consider v being Vertex of G such that
A4: ( E = v .edgesOut() & v in X ) by A3;
( e in the_Edges_of G & (the_Source_of G) . e = v ) by A3, A4, Lm8;
hence e in G .edgesOutOf X by A4, Def27; :: thesis: verum

end;

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