theorem :: GLIBPRE0:37

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