theorem :: GLIB_000:160

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