theorem :: GLIBPRE0:36

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