theorem :: GLIB_000:17

for G being _Graph
for X, Y being set
for e, x, y being object st e Joins x,y,G & ( ( x in X & y in Y ) or ( x in Y & y in X ) ) holds
e SJoins X,Y,G ;