theorem Th162: :: GLIB_000:162

for G being _Graph
for X, Y being set holds G .edgesBetween (X,Y) c= union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) }